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  1414  peano5  4903  funopg  5520  eldmrexrnb  5913  f1o2ndf1  6490  abianfp  6752  omordi  6845  omeulem1  6861  brecop  7033  isinf  7358  fiint  7419  carduni  7906  dfac5  8047  dfac2  8049  cofsmo  8187  cfcoflem  8190  domtriomlem  8360  axdc3lem2  8369  nqereu  8844  squeeze0  9951  zmax  10609  xrsupsslem  10923  xrinfmsslem  10924  supxrunb1  10936  supxrunb2  10937  difreicc  11066  elfznelfzo  11230  injresinjlem  11237  injresinj  11238  uzindi  11358  facwordi  11618  hasheqf1oi  11673  hashf1rn  11674  hash2prde  11726  sqr2irr  12886  spwmo  14696  bwth  17511  fbunfip  17939  usgranloopv  21436  usgraedg4  21444  usgraidx2vlem2  21449  usgrafisbase  21466  nbgra0nb  21479  nbgraf1olem3  21491  nbgraf1olem5  21493  nbcusgra  21510  cusgrasize2inds  21524  cusgrafi  21529  usgrasscusgra  21530  sizeusglecusglem1  21531  sizeusglecusg  21533  uvtxnbgra  21540  spthonepeq  21625  1pthoncl  21630  wlkdvspthlem  21645  cyclnspth  21656  fargshiftf1  21662  usgrcyclnl2  21666  nvnencycllem  21668  3v3e3cycl1  21669  4cycl4v4e  21691  4cycl4dv4e  21693  hashnbgravdg  21720  grpomndo  21972  rngoueqz  22056  zerdivemp1  22060  rngoridfz  22061  shmodsi  22929  kbass6  23662  mdsymlem6  23949  mdsymlem7  23950  cdj3lem2a  23977  cdj3lem3a  23980  predpo  25494  zerdivemp1x  26613  psgnunilem4  27509  funressnfv  28080  funbrafv  28110  otiunsndisj  28179  otiunsndisjX  28180  ssfz12  28225  elfzelfzelfz  28230  elfz0fzfz0  28235  fz0fzelfz0  28239  fz0fzdiffz0  28240  ubmelfzo  28247  ubmelm1fzo  28248  fzo1fzo0n0  28249  ssfzo12  28251  fzoopth  28260  swrdnd  28314  swrdvalodm2  28320  swrd0swrd  28329  swrdswrdlem  28330  swrdswrd  28331  swrdccatin1  28337  swrdccatin12lem3  28344  swrdccat  28348  2cshw1lem2  28381  2cshw  28388  2cshwmod  28389  cshweqdif2s  28403  cshweqrep  28406  cshwssizelem1a  28411  usg2wlkeq  28440  usgra2pthspth  28441  usgra2wlkspthlem1  28442  usgra2wlkspth  28444  usgra2pth  28447  usgra2adedgspthlem2  28450  el2wlkonotot0  28502  usg2wlkonot  28513  usg2wotspth  28514  usgfidegfi  28523  frgraunss  28557  frgra3vlem1  28562  3cyclfrgrarn1  28574  3cyclfrgrarn  28575  4cycl2vnunb  28579  frgranbnb  28582  vdn0frgrav2  28586  vdn1frgrav2  28588  frgrancvvdeqlemB  28599  frgrawopreglem2  28606  frg2wot1  28618  usg2spot2nb  28626  2spotmdisj  28629  3imp31  28826  eel12131  28993  tratrbVD  29147  2uasbanhVD  29197  elpcliN  30864
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
  Copyright terms: Public domain W3C validator