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

Theorem com13 88
 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 87 . 2 (𝜒 → (𝜑 → (𝜓𝜃)))
32com23 86 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  95  an13s  650  an31s  653  3imp31  1109  3imp21  1111  meredith  1643  preqsnd  4752  3elpr2eq  4802  propeqop  5365  po2ne  5457  predpo  6138  funopg  6362  eldmrexrnb  6839  fvn0fvelrn  6906  peano5  7589  f1o2ndf1  7805  suppimacnv  7828  omordi  8179  omeulem1  8195  brecop  8377  isinf  8719  fiint  8783  carduni  9398  dfac5  9543  dfac2b  9545  cofsmo  9684  cfcoflem  9687  domtriomlem  9857  axdc3lem2  9866  nqereu  10344  squeeze0  11536  zmax  12337  elpq  12366  xnn0lenn0nn0  12630  xrsupsslem  12692  xrinfmsslem  12693  supxrunb1  12704  supxrunb2  12705  difreicc  12866  elfz0ubfz0  13010  elfz0fzfz0  13011  fz0fzelfz0  13012  fz0fzdiffz0  13015  fzo1fzo0n0  13087  elfzodifsumelfzo  13102  ssfzo12  13129  ssfzo12bi  13131  elfznelfzo  13141  injresinjlem  13156  injresinj  13157  addmodlteq  13313  uzindi  13349  ssnn0fi  13352  suppssfz  13361  facwordi  13649  hasheqf1oi  13712  hashf1rn  13713  fundmge2nop0  13850  swrdswrdlem  14061  swrdswrd  14062  wrd2ind  14080  swrdccatin1  14082  pfxccatin12lem2  14088  swrdccat  14092  reuccatpfxs1lem  14103  repsdf2  14135  cshwidx0  14163  cshweqrep  14178  2cshwcshw  14182  cshwcsh2id  14185  swrdco  14194  wwlktovfo  14317  sqrt2irr  15597  oddnn02np1  15692  oddge22np1  15693  evennn02n  15694  evennn2n  15695  dfgcd2  15887  lcmf  15970  lcmfunsnlem2lem2  15976  initoeu2lem1  17269  symgfix2  18539  gsmsymgreqlem2  18554  psgnunilem4  18620  lmodfopnelem1  19666  01eq0ring  20041  cply1mul  20926  gsummoncoe1  20936  mamufacex  20999  matecl  21033  gsummatr01  21267  mp2pm2mplem4  21417  chfacfscmul0  21466  chfacfpmmul0  21470  cayhamlem1  21474  fbunfip  22477  tngngp3  23265  zabsle1  25883  gausslemma2dlem1a  25952  2lgsoddprm  26003  2sqreunnltblem  26038  umgrnloopv  26902  upgredg2vtx  26937  usgruspgrb  26977  usgrnloopvALT  26994  usgredg2vlem2  27019  edg0usgr  27046  nbuhgr  27136  nbumgr  27140  nbuhgr2vtx1edgblem  27144  cusgredg  27217  cusgrsize2inds  27246  sizusglecusg  27256  umgr2v2enb1  27319  rusgr1vtx  27381  uspgr2wlkeq  27438  wlkreslem  27462  spthonepeq  27544  usgr2trlspth  27553  clwlkl1loop  27575  lfgrn1cycl  27594  uspgrn2crct  27597  crctcshwlkn0lem3  27601  crctcshwlkn0lem5  27603  wwlksnextbi  27683  wwlksnredwwlkn0  27685  wwlksnextinj  27688  wspthsnonn0vne  27706  umgr2adedgspth  27737  umgr2wlk  27738  usgr2wspthons3  27753  clwlkclwwlklem2a1  27780  clwlkclwwlklem2fv2  27784  clwlkclwwlklem2a4  27785  clwlkclwwlklem2a  27786  clwlkclwwlklem2  27788  clwwisshclwws  27803  erclwwlktr  27810  clwwlkn1loopb  27831  clwwlknwwlksnb  27843  clwwlkext2edg  27844  erclwwlkntr  27859  clwwlknon1  27885  clwwlknonwwlknonb  27894  clwwlknonex2lem2  27896  upgr1wlkdlem1  27933  upgr3v3e3cycl  27968  uhgr3cyclex  27970  upgr4cycl4dv4e  27973  eucrctshift  28031  frgr3vlem1  28061  3cyclfrgrrn1  28073  3cyclfrgrrn  28074  4cycl2vnunb  28078  frgrnbnb  28081  frgrncvvdeqlem8  28094  frgrwopreglem5  28109  frgrwopreglem5ALT  28110  frgr2wwlk1  28117  2clwwlk2clwwlk  28138  numclwwlk1lem2fo  28146  frgrreg  28182  friendshipgt3  28186  shmodsi  29175  kbass6  29907  mdsymlem6  30194  mdsymlem7  30195  cdj3lem2a  30222  cdj3lem3a  30225  satfrel  32722  gonarlem  32749  satffunlem1lem1  32757  satffunlem2lem1  32759  satffun  32764  wl-spae  34919  grpomndo  35306  rngoueqz  35371  zerdivemp1x  35378  elpcliN  37182  relexpiidm  40392  relexpxpmin  40405  ntrk0kbimka  40729  eel12131  41406  tratrbVD  41554  2uasbanhVD  41604  funressnfv  43622  funbrafv  43701  otiunsndisjX  43822  ssfz12  43858  fzoopth  43871  iccpartgt  43931  iccelpart  43937  iccpartnel  43942  fargshiftf1  43945  sprsymrelfvlem  43994  sprsymrelf1lem  43995  prproropf1olem4  44010  sbcpr  44025  reupr  44026  poprelb  44028  reuopreuprim  44030  fmtno4prmfac  44076  lighneallem4b  44114  lighneal  44116  mogoldbblem  44225  gbegt5  44266  sbgoldbaltlem1  44284  sbgoldbm  44289  bgoldbtbndlem2  44311  bgoldbtbndlem3  44312  bgoldbtbndlem4  44313  bgoldbtbnd  44314  isomuspgrlem2b  44334  isomuspgrlem2d  44336  lidldomn1  44532  2zrngamgm  44550  rngccatidALTV  44600  ringccatidALTV  44663  nzerooringczr  44683  scmsuppss  44761  ply1mulgsumlem1  44781  lincsumcl  44827  ellcoellss  44831  lindslinindsimp1  44853  lindslinindimp2lem1  44854  nn0sumshdiglemA  45020  nn0sumshdiglemB  45021  itschlc0xyqsol1  45167
 Copyright terms: Public domain W3C validator