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

Theorem com13 86
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 85 . 2 (𝜒 → (𝜑 → (𝜓𝜃)))
32com23 84 1 (𝜒 → (𝜓 → (𝜑𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  com24  93  imim12  103  an13s  841  an31s  844  3imp31  1250  meredith  1557  propeqop  4895  predpo  5615  funopg  5836  eldmrexrnb  6274  fvn0fvelrn  6335  peano5  6981  f1o2ndf1  7172  suppimacnv  7193  omordi  7533  omeulem1  7549  brecop  7727  isinf  8058  fiint  8122  carduni  8690  dfac5  8834  dfac2  8836  cofsmo  8974  cfcoflem  8977  domtriomlem  9147  axdc3lem2  9156  nqereu  9630  squeeze0  10805  zmax  11661  xrsupsslem  12009  xrinfmsslem  12010  supxrunb1  12021  supxrunb2  12022  difreicc  12175  elfz0ubfz0  12312  elfz0fzfz0  12313  fz0fzelfz0  12314  fz0fzdiffz0  12317  fzo1fzo0n0  12386  elfzodifsumelfzo  12401  ssfzo12  12427  ssfzo12bi  12429  elfznelfzo  12439  injresinjlem  12450  injresinj  12451  addmodlteq  12607  uzindi  12643  ssnn0fi  12646  suppssfz  12656  facwordi  12938  hasheqf1oi  13002  hasheqf1oiOLD  13003  hashf1rn  13004  hashf1rnOLD  13005  hash2prde  13109  fundmge2nop0  13129  swrdswrdlem  13311  swrdswrd  13312  wrd2ind  13329  reuccats1lem  13331  swrdccatin1  13334  swrdccatin12lem2  13340  swrdccat  13344  repsdf2  13376  cshwidx0  13403  cshweqrep  13418  2cshwcshw  13422  cshwcsh2id  13425  swrdco  13434  wwlktovfo  13549  sqrt2irr  14817  oddnn02np1  14910  oddge22np1  14911  evennn02n  14912  evennn2n  14913  dfgcd2  15101  lcmf  15184  lcmfunsnlem2lem2  15190  initoeu2lem1  16487  symgfix2  17659  gsmsymgreqlem2  17674  psgnunilem4  17740  lmodfopnelem1  18722  01eq0ring  19093  cply1mul  19485  gsummoncoe1  19495  mamufacex  20014  matecl  20050  gsummatr01lem4  20283  gsummatr01  20284  mp2pm2mplem4  20433  chfacfscmul0  20482  chfacfpmmul0  20486  cayhamlem1  20490  fbunfip  21483  tngngp3  22270  zabsle1  24821  gausslemma2dlem1a  24890  2lgsoddprm  24941  umgrnloopv  25772  upgredg2vtx  25814  usgranloopv  25907  usgraedg4  25916  usgraidx2vlem2  25921  usgrafisbase  25943  nbgra0nb  25958  nbgraf1olem3  25972  nbgraf1olem5  25974  nbcusgra  25992  cusgrasize2inds  26005  cusgrafi  26010  usgrasscusgra  26011  sizeusglecusglem1  26012  sizeusglecusg  26014  uvtxnbgra  26021  spthonepeq  26117  1pthoncl  26122  wlkdvspthlem  26137  usgra2adedgspthlem2  26140  usgra2wlkspthlem1  26147  usgra2wlkspth  26149  cyclnspth  26159  fargshiftf1  26165  usgrcyclnl2  26169  nvnencycllem  26171  3v3e3cycl1  26172  4cycl4v4e  26194  4cycl4dv4e  26196  usg2wlkeq  26236  wwlknextbi  26253  wwlknredwwlkn0  26255  wwlkextinj  26258  clwwlkgt0  26299  clwlkisclwwlklem2a1  26307  clwlkisclwwlklem2fv2  26311  clwlkisclwwlklem2a4  26312  clwlkisclwwlklem2a  26313  clwlkisclwwlklem1  26315  clwwlkext2edg  26330  clwwisshclww  26335  erclwwlktr  26343  usg2cwwk2dif  26348  erclwwlkntr  26355  clwlkf1clwwlklem  26376  el2wlkonotot0  26399  usg2wlkonot  26410  usg2wotspth  26411  usgfidegfi  26437  hashnbgravdg  26440  frgraunss  26522  frgra3vlem1  26527  3cyclfrgrarn1  26539  3cyclfrgrarn  26540  4cycl2vnunb  26544  frgranbnb  26547  vdn0frgrav2  26550  vdn1frgrav2  26552  usgn0fidegnn0  26556  frgrancvvdeqlemB  26565  frgrawopreglem2  26572  frg2wot1  26584  usg2spot2nb  26592  2spotmdisj  26595  clwwlkextfrlem1  26603  extwwlkfablem2  26605  numclwlk1lem2fo  26622  frgrareggt1  26643  frgrareg  26644  friendshipgt3  26648  shmodsi  27632  kbass6  28364  mdsymlem6  28651  mdsymlem7  28652  cdj3lem2a  28679  cdj3lem3a  28682  wl-spae  32485  grpomndo  32844  rngoueqz  32909  zerdivemp1x  32916  elpcliN  34197  relexpiidm  37015  relexpxpmin  37028  ntrk0kbimka  37357  eel12131  37959  tratrbVD  38119  2uasbanhVD  38169  funressnfv  39857  funbrafv  39887  iccpartgt  39965  iccelpart  39971  iccpartnel  39976  fmtno4prmfac  40022  lighneallem4b  40064  lighneal  40066  gbegt5  40183  sgoldbaltlem1  40201  bgoldbtbndlem2  40222  bgoldbtbndlem3  40223  bgoldbtbndlem4  40224  bgoldbtbnd  40225  pfxccatin12lem2  40287  reuccatpfxs1lem  40296  reuccatpfxs1  40297  otiunsndisjX  40317  ssfz12  40351  fzoopth  40360  usgruspgrb  40411  usgrnloopvALT  40428  usgredg2vlem2  40453  edg0usgr  40479  nbuhgr  40565  nbumgr  40569  nbuhgr2vtx1edgblem  40573  cusgredg  40646  cusgrsize2inds  40669  sizusglecusg  40679  umgr2v2enb1  40742  rusgr1vtx  40788  upgrewlkle2  40808  uspgr2wlkeq  40854  1wlkreslem  40878  spthonepeq-av  40958  usgr2wlkneq  40962  usgr2trlspth  40967  usgr2pth  40970  clwlkl1loop  40989  lfgrn1cycl  41008  uspgrn2crct  41011  crctcsh1wlkn0lem3  41015  crctcsh1wlkn0lem5  41017  wwlksnextbi  41100  wwlksnredwwlkn0  41102  wwlksnextinj  41105  wspthsnonn0vne  41124  umgr2adedgspth  41155  umgr2wlk  41156  usgr2wspthons3  41167  clwlkclwwlklem2a1  41201  clwlkclwwlklem2fv2  41205  clwlkclwwlklem2a4  41206  clwlkclwwlklem2a  41207  clwlkclwwlklem2  41209  clwwlksext2edg  41230  clwwisshclwws  41235  erclwwlkstr  41243  erclwwlksntr  41255  upgr11wlkdlem1  41312  upgr3v3e3cycl  41347  uhgr3cyclex  41349  upgr4cycl4dv4e  41352  eucrctshift  41411  frgr3vlem1  41443  3cyclfrgrrn1  41455  3cyclfrgrrn  41456  4cycl2vnunb-av  41460  frgrnbnb  41463  frgrncvvdeqlemB  41477  frgr2wwlk1  41494  av-numclwwlkffin0  41513  av-numclwlk1lem2fo  41525  av-frgrareg  41548  av-friendshipgt3  41552  lidldomn1  41711  2zrngamgm  41729  rngccatidALTV  41781  ringccatidALTV  41844  nzerooringczr  41864  scmsuppss  41947  ply1mulgsumlem1  41968  lincsumcl  42014  ellcoellss  42018  lindslinindsimp1  42040  lindslinindimp2lem1  42041  nn0sumshdiglemA  42211  nn0sumshdiglemB  42212
  Copyright terms: Public domain W3C validator