MPE Home 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  647  an31s  650  3imp31  1104  3imp21  1106  meredith  1633  preqsnd  4781  3elpr2eq  4829  propeqop  5388  po2ne  5482  predpo  6159  funopg  6382  eldmrexrnb  6850  fvn0fvelrn  6917  peano5  7594  f1o2ndf1  7807  suppimacnv  7830  omordi  8181  omeulem1  8197  brecop  8379  isinf  8719  fiint  8783  carduni  9398  dfac5  9542  dfac2b  9544  cofsmo  9679  cfcoflem  9682  domtriomlem  9852  axdc3lem2  9861  nqereu  10339  squeeze0  11531  zmax  12333  elpq  12362  xnn0lenn0nn0  12626  xrsupsslem  12688  xrinfmsslem  12689  supxrunb1  12700  supxrunb2  12701  difreicc  12858  elfz0ubfz0  12999  elfz0fzfz0  13000  fz0fzelfz0  13001  fz0fzdiffz0  13004  fzo1fzo0n0  13076  elfzodifsumelfzo  13091  ssfzo12  13118  ssfzo12bi  13120  elfznelfzo  13130  injresinjlem  13145  injresinj  13146  addmodlteq  13302  uzindi  13338  ssnn0fi  13341  suppssfz  13350  facwordi  13637  hasheqf1oi  13700  hashf1rn  13701  fundmge2nop0  13838  swrdswrdlem  14054  swrdswrd  14055  wrd2ind  14073  swrdccatin1  14075  pfxccatin12lem2  14081  swrdccat  14085  reuccatpfxs1lem  14096  repsdf2  14128  cshwidx0  14156  cshweqrep  14171  2cshwcshw  14175  cshwcsh2id  14178  swrdco  14187  wwlktovfo  14310  sqrt2irr  15590  oddnn02np1  15685  oddge22np1  15686  evennn02n  15687  evennn2n  15688  dfgcd2  15882  lcmf  15965  lcmfunsnlem2lem2  15971  initoeu2lem1  17262  symgfix2  18473  gsmsymgreqlem2  18488  psgnunilem4  18554  lmodfopnelem1  19599  01eq0ring  19973  cply1mul  20390  gsummoncoe1  20400  mamufacex  20928  matecl  20962  gsummatr01  21196  mp2pm2mplem4  21345  chfacfscmul0  21394  chfacfpmmul0  21398  cayhamlem1  21402  fbunfip  22405  tngngp3  23192  zabsle1  25799  gausslemma2dlem1a  25868  2lgsoddprm  25919  2sqreunnltblem  25954  umgrnloopv  26818  upgredg2vtx  26853  usgruspgrb  26893  usgrnloopvALT  26910  usgredg2vlem2  26935  edg0usgr  26962  nbuhgr  27052  nbumgr  27056  nbuhgr2vtx1edgblem  27060  cusgredg  27133  cusgrsize2inds  27162  sizusglecusg  27172  umgr2v2enb1  27235  rusgr1vtx  27297  uspgr2wlkeq  27354  wlkreslem  27378  spthonepeq  27460  usgr2trlspth  27469  clwlkl1loop  27491  lfgrn1cycl  27510  uspgrn2crct  27513  crctcshwlkn0lem3  27517  crctcshwlkn0lem5  27519  wwlksnextbi  27599  wwlksnredwwlkn0  27601  wwlksnextinj  27604  wspthsnonn0vne  27623  umgr2adedgspth  27654  umgr2wlk  27655  usgr2wspthons3  27670  clwlkclwwlklem2a1  27697  clwlkclwwlklem2fv2  27701  clwlkclwwlklem2a4  27702  clwlkclwwlklem2a  27703  clwlkclwwlklem2  27705  clwwisshclwws  27720  erclwwlktr  27727  clwwlkn1loopb  27748  clwwlknwwlksnb  27761  clwwlkext2edg  27762  erclwwlkntr  27777  clwwlknon1  27803  clwwlknonwwlknonb  27812  clwwlknonex2lem2  27814  upgr1wlkdlem1  27851  upgr3v3e3cycl  27886  uhgr3cyclex  27888  upgr4cycl4dv4e  27891  eucrctshift  27949  frgr3vlem1  27979  3cyclfrgrrn1  27991  3cyclfrgrrn  27992  4cycl2vnunb  27996  frgrnbnb  27999  frgrncvvdeqlem8  28012  frgrwopreglem5  28027  frgrwopreglem5ALT  28028  frgr2wwlk1  28035  2clwwlk2clwwlk  28056  numclwwlk1lem2fo  28064  frgrreg  28100  friendshipgt3  28104  shmodsi  29093  kbass6  29825  mdsymlem6  30112  mdsymlem7  30113  cdj3lem2a  30140  cdj3lem3a  30143  satfrel  32511  gonarlem  32538  satffunlem1lem1  32546  satffunlem2lem1  32548  satffun  32553  bj-snmoore  34299  wl-spae  34643  grpomndo  35034  rngoueqz  35099  zerdivemp1x  35106  elpcliN  36909  relexpiidm  39927  relexpxpmin  39940  ntrk0kbimka  40267  eel12131  40924  tratrbVD  41072  2uasbanhVD  41122  funressnfv  43155  funbrafv  43234  otiunsndisjX  43355  ssfz12  43391  fzoopth  43404  iccpartgt  43464  iccelpart  43470  iccpartnel  43475  fargshiftf1  43478  sprsymrelfvlem  43529  sprsymrelf1lem  43530  prproropf1olem4  43545  sbcpr  43560  reupr  43561  poprelb  43563  reuopreuprim  43565  fmtno4prmfac  43611  lighneallem4b  43651  lighneal  43653  mogoldbblem  43762  gbegt5  43803  sbgoldbaltlem1  43821  sbgoldbm  43826  bgoldbtbndlem2  43848  bgoldbtbndlem3  43849  bgoldbtbndlem4  43850  bgoldbtbnd  43851  isomuspgrlem2b  43871  isomuspgrlem2d  43873  lidldomn1  44120  2zrngamgm  44138  rngccatidALTV  44188  ringccatidALTV  44251  nzerooringczr  44271  scmsuppss  44348  ply1mulgsumlem1  44368  lincsumcl  44414  ellcoellss  44418  lindslinindsimp1  44440  lindslinindimp2lem1  44441  nn0sumshdiglemA  44607  nn0sumshdiglemB  44608  itschlc0xyqsol1  44681
  Copyright terms: Public domain W3C validator