MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  com13 Structured version   GIF version

Theorem com13 77
Description: Commutation of antecedents. Swap 1st and 3rd. (Contributed by NM, 25-Apr-1994.) (Proof shortened by Wolf Lammen, 28-Jul-2012.)
Hypothesis
Ref Expression
com3.1 (𝜑 → (𝜓 → (𝜒𝜃)))
Assertion
Ref Expression
com13 (𝜒 → (𝜓 → (𝜑𝜃)))

Proof of Theorem com13
StepHypRef Expression
1 com3.1 . . 3 (𝜑 → (𝜓 → (𝜒𝜃)))
21com3r 76 . 2 (𝜒 → (𝜑 → (𝜓𝜃)))
32com23 75 1 (𝜒 → (𝜓 → (𝜑𝜃)))
Colors of variables: wff set class
Syntax hints:  wi 4
This theorem is referenced by:  com24  84  an13s  780  an31s  783  meredith  1420  peano5  4960  funopg  5584  eldmrexrnb  5977  f1o2ndf1  6558  abianfp  6811  omordi  6904  omeulem1  6920  brecop  7092  isinf  7417  fiint  7478  carduni  7965  dfac5  8106  dfac2  8108  cofsmo  8246  cfcoflem  8249  domtriomlem  8419  axdc3lem2  8428  nqereu  8903  squeeze0  10011  zmax  10671  xrsupsslem  10985  xrinfmsslem  10986  supxrunb1  10998  supxrunb2  10999  difreicc  11128  elfznelfzo  11294  injresinjlem  11301  injresinj  11302  uzindi  11424  facwordi  11684  hasheqf1oi  11739  hashf1rn  11740  hash2prde  11792  sqr2irr  12968  bwth  17605  fbunfip  18033  usgranloopv  21530  usgraedg4  21538  usgraidx2vlem2  21543  usgrafisbase  21560  nbgra0nb  21573  nbgraf1olem3  21585  nbgraf1olem5  21587  nbcusgra  21604  cusgrasize2inds  21618  cusgrafi  21623  usgrasscusgra  21624  sizeusglecusglem1  21625  sizeusglecusg  21627  uvtxnbgra  21634  spthonepeq  21719  1pthoncl  21724  wlkdvspthlem  21739  cyclnspth  21750  fargshiftf1  21756  usgrcyclnl2  21760  nvnencycllem  21762  3v3e3cycl1  21763  4cycl4v4e  21785  4cycl4dv4e  21787  hashnbgravdg  21814  grpomndo  22066  rngoueqz  22150  zerdivemp1  22154  rngoridfz  22155  shmodsi  23023  kbass6  23756  mdsymlem6  24043  mdsymlem7  24044  cdj3lem2a  24071  cdj3lem3a  24074  predpo  25916  zerdivemp1x  27027  psgnunilem4  27919  funressnfv  28487  funbrafv  28517  otiunsndisj  28591  otiunsndisjX  28592  fvn0fvelrn  28616  ssfz12  28666  elfzelfzelfz  28671  elfz0fzfz0  28676  fz0fzelfz0  28680  fz0fzdiffz0  28681  ubmelfzo  28694  ubmelm1fzo  28695  fzo1fzo0n0  28696  ssfzo12  28698  fzoopth  28706  wwlktovsur  28804  swrdnd  28830  swrdvalodm2  28836  swrd0swrd  28847  swrdswrdlem  28848  swrdswrd  28849  swrdccatin1  28868  swrdccatin12lem3  28875  swrdccat  28879  2cshw1lem2  28921  2cshw  28928  2cshwmod  28929  cshweqdif2s  28936  cshweqrep  28939  cshwssizelem1a  28944  usg2wlkeq  28973  usgra2pthspth  28979  usgra2wlkspthlem1  28980  usgra2wlkspth  28982  usgra2pth  28985  usgra2adedgspthlem2  28988  wwlknextbi  29041  wwlknredwwlkn0  29043  wwlkextinj  29046  el2wlkonotot0  29075  usg2wlkonot  29086  usg2wotspth  29087  clwwlkgt0  29118  clwlkisclwwlklem2a1  29125  clwlkisclwwlklem2fv2  29129  clwlkisclwwlklem2a4  29130  clwlkisclwwlklem2a  29131  clwlkisclwwlklem1  29133  clwwlkext2edg  29148  clwwisshclwwlem3  29164  clwwisshclww  29166  erclwwlktr0  29174  erclwwlktr  29180  cshwlemma1  29184  usg2cwwk2dif  29189  erclwwlkntr  29196  clwlkf1clwwlklem  29217  usgfidegfi  29222  frgraunss  29282  frgra3vlem1  29287  3cyclfrgrarn1  29299  3cyclfrgrarn  29300  4cycl2vnunb  29304  frgranbnb  29307  vdn0frgrav2  29311  vdn1frgrav2  29313  usgn0fidegnn0  29317  frgrancvvdeqlemB  29326  frgrawopreglem2  29333  frg2wot1  29345  usg2spot2nb  29353  2spotmdisj  29356  clwwlkextfrlem1  29364  extwwlkfablem2  29366  numclwlk1lem2fo  29383  frgrareggt1  29404  frgrareg  29405  friendshipgt3  29409  3imp31  29620  eel12131  29787  tratrbVD  29941  2uasbanhVD  29991  elpcliN  31739
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
  Copyright terms: Public domain W3C validator