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  4783  3elpr2eq  4831  propeqop  5389  po2ne  5483  predpo  6160  funopg  6383  eldmrexrnb  6851  fvn0fvelrn  6918  peano5  7593  f1o2ndf1  7809  suppimacnv  7832  omordi  8182  omeulem1  8198  brecop  8380  isinf  8720  fiint  8784  carduni  9399  dfac5  9543  dfac2b  9545  cofsmo  9680  cfcoflem  9683  domtriomlem  9853  axdc3lem2  9862  nqereu  10340  squeeze0  11532  zmax  12334  elpq  12364  xnn0lenn0nn0  12628  xrsupsslem  12690  xrinfmsslem  12691  supxrunb1  12702  supxrunb2  12703  difreicc  12860  elfz0ubfz0  13001  elfz0fzfz0  13002  fz0fzelfz0  13003  fz0fzdiffz0  13006  fzo1fzo0n0  13078  elfzodifsumelfzo  13093  ssfzo12  13120  ssfzo12bi  13122  elfznelfzo  13132  injresinjlem  13147  injresinj  13148  addmodlteq  13304  uzindi  13340  ssnn0fi  13343  suppssfz  13352  facwordi  13639  hasheqf1oi  13702  hashf1rn  13703  fundmge2nop0  13840  swrdswrdlem  14056  swrdswrd  14057  wrd2ind  14075  swrdccatin1  14077  pfxccatin12lem2  14083  swrdccat  14087  reuccatpfxs1lem  14098  repsdf2  14130  cshwidx0  14158  cshweqrep  14173  2cshwcshw  14177  cshwcsh2id  14180  swrdco  14189  wwlktovfo  14312  sqrt2irr  15592  oddnn02np1  15687  oddge22np1  15688  evennn02n  15689  evennn2n  15690  dfgcd2  15884  lcmf  15967  lcmfunsnlem2lem2  15973  initoeu2lem1  17264  symgfix2  18475  gsmsymgreqlem2  18490  psgnunilem4  18556  lmodfopnelem1  19601  01eq0ring  19975  cply1mul  20392  gsummoncoe1  20402  mamufacex  20930  matecl  20964  gsummatr01  21198  mp2pm2mplem4  21347  chfacfscmul0  21396  chfacfpmmul0  21400  cayhamlem1  21404  fbunfip  22407  tngngp3  23194  zabsle1  25800  gausslemma2dlem1a  25869  2lgsoddprm  25920  2sqreunnltblem  25955  umgrnloopv  26819  upgredg2vtx  26854  usgruspgrb  26894  usgrnloopvALT  26911  usgredg2vlem2  26936  edg0usgr  26963  nbuhgr  27053  nbumgr  27057  nbuhgr2vtx1edgblem  27061  cusgredg  27134  cusgrsize2inds  27163  sizusglecusg  27173  umgr2v2enb1  27236  rusgr1vtx  27298  uspgr2wlkeq  27355  wlkreslem  27379  spthonepeq  27461  usgr2trlspth  27470  clwlkl1loop  27492  lfgrn1cycl  27511  uspgrn2crct  27514  crctcshwlkn0lem3  27518  crctcshwlkn0lem5  27520  wwlksnextbi  27600  wwlksnredwwlkn0  27602  wwlksnextinj  27605  wspthsnonn0vne  27624  umgr2adedgspth  27655  umgr2wlk  27656  usgr2wspthons3  27671  clwlkclwwlklem2a1  27698  clwlkclwwlklem2fv2  27702  clwlkclwwlklem2a4  27703  clwlkclwwlklem2a  27704  clwlkclwwlklem2  27706  clwwisshclwws  27721  erclwwlktr  27728  clwwlkn1loopb  27749  clwwlknwwlksnb  27762  clwwlkext2edg  27763  erclwwlkntr  27778  clwwlknon1  27804  clwwlknonwwlknonb  27813  clwwlknonex2lem2  27815  upgr1wlkdlem1  27852  upgr3v3e3cycl  27887  uhgr3cyclex  27889  upgr4cycl4dv4e  27892  eucrctshift  27950  frgr3vlem1  27980  3cyclfrgrrn1  27992  3cyclfrgrrn  27993  4cycl2vnunb  27997  frgrnbnb  28000  frgrncvvdeqlem8  28013  frgrwopreglem5  28028  frgrwopreglem5ALT  28029  frgr2wwlk1  28036  2clwwlk2clwwlk  28057  numclwwlk1lem2fo  28065  frgrreg  28101  friendshipgt3  28105  shmodsi  29094  kbass6  29826  mdsymlem6  30113  mdsymlem7  30114  cdj3lem2a  30141  cdj3lem3a  30144  satfrel  32512  gonarlem  32539  satffunlem1lem1  32547  satffunlem2lem1  32549  satffun  32554  bj-snmoore  34300  wl-spae  34644  grpomndo  35036  rngoueqz  35101  zerdivemp1x  35108  elpcliN  36911  relexpiidm  39929  relexpxpmin  39942  ntrk0kbimka  40269  eel12131  40927  tratrbVD  41075  2uasbanhVD  41125  funressnfv  43159  funbrafv  43238  otiunsndisjX  43359  ssfz12  43395  fzoopth  43408  iccpartgt  43434  iccelpart  43440  iccpartnel  43445  fargshiftf1  43448  sprsymrelfvlem  43499  sprsymrelf1lem  43500  prproropf1olem4  43515  sbcpr  43530  reupr  43531  poprelb  43533  reuopreuprim  43535  fmtno4prmfac  43581  lighneallem4b  43621  lighneal  43623  mogoldbblem  43732  gbegt5  43773  sbgoldbaltlem1  43791  sbgoldbm  43796  bgoldbtbndlem2  43818  bgoldbtbndlem3  43819  bgoldbtbndlem4  43820  bgoldbtbnd  43821  isomuspgrlem2b  43841  isomuspgrlem2d  43843  lidldomn1  44090  2zrngamgm  44108  rngccatidALTV  44158  ringccatidALTV  44221  nzerooringczr  44241  scmsuppss  44318  ply1mulgsumlem1  44338  lincsumcl  44384  ellcoellss  44388  lindslinindsimp1  44410  lindslinindimp2lem1  44411  nn0sumshdiglemA  44577  nn0sumshdiglemB  44578  itschlc0xyqsol1  44651
  Copyright terms: Public domain W3C validator