Theorem com13 89

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

Step	Hyp	Ref	Expression
1		com3.1	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
2	1	com3r 88	. 2 ⊢ (𝜒 → (𝜑 → (𝜓 → 𝜃)))
3	2	com23 87	1 ⊢ (𝜒 → (𝜓 → (𝜑 → 𝜃)))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  com24  96  an13s  664  an31s  667  3imp31  1129  3imp21  1131  meredith  1674  preqsnd  4829  3elpr2eq  4876  propeqop  5495  po2ne  5590  funopg  6577  eldmrexrnb  7094  peano5  7899  f1o2ndf1  8126  suppimacnv  8179  omordi  8560  omeulem1  8576  brecop  8817  isinf  9235  fiint  9296  carduni  9986  dfac5  10131  dfac2b  10133  cofsmo  10271  cfcoflem  10274  domtriomlem  10444  axdc3lem2  10453  nqereu  10932  squeeze0  12136  zmax  12987  elpq  13017  xnn0lenn0nn0  13289  xrsupsslem  13351  xrinfmsslem  13352  supxrunb1  13363  supxrunb2  13364  difreicc  13529  elfz0ubfz0  13679  elfz0fzfz0  13680  fz0fzelfz0  13681  fz0fzdiffz0  13684  fzo1fzo0n0  13763  elfzodifsumelfzo  13779  ssfzo12  13807  ssfzo12bi  13809  fzoopth  13810  elfznelfzo  13821  injresinjlem  13838  injresinj  13839  addmodlteq  14002  uzindi  14038  ssnn0fi  14041  suppssfz  14050  facwordi  14345  hasheqf1oi  14407  hashf1rn  14408  fundmge2nop0  14559  swrdswrdlem  14765  swrdswrd  14766  wrd2ind  14784  swrdccatin1  14786  pfxccatin12lem2  14792  swrdccat  14796  reuccatpfxs1lem  14807  repsdf2  14841  cshwidx0  14869  cshweqrep  14884  2cshwcshw  14888  cshwcsh2id  14891  swrdco  14900  wwlktovfo  15021  sqrt2irr  16330  oddnn02np1  16431  oddge22np1  16432  evennn02n  16433  evennn2n  16434  dfgcd2  16629  lcmf  16716  lcmfunsnlem2lem2  16722  initoeu2lem1  18096  symgfix2  19517  gsmsymgreqlem2  19532  psgnunilem4  19598  01eq0ringOLD  20666  lmodfopnelem1  21056  nzerooringczr  21667  cply1mul  22493  gsummoncoe1  22505  mamufacex  22590  matecl  22619  gsummatr01  22853  mp2pm2mplem4  23003  chfacfscmul0  23052  chfacfpmmul0  23056  cayhamlem1  23060  fbunfip  24063  tngngp3  24850  mpomulcn  25063  zabsle1  27497  gausslemma2dlem1a  27566  2lgsoddprm  27617  2sqreunnltblem  27652  umgrnloopv  29493  upgredg2vtx  29528  usgruspgrb  29570  usgrnloopvALT  29588  usgredg2vlem2  29613  edg0usgr  29640  nbuhgr  29730  nbumgr  29734  nbuhgr2vtx1edgblem  29738  cusgredg  29811  cusgrsize2inds  29840  sizusglecusg  29850  umgr2v2enb1  29913  rusgr1vtx  29975  uspgr2wlkeq  30032  wlkreslem  30054  spthonepeq  30138  usgr2trlspth  30147  clwlkl1loop  30169  lfgrn1cycl  30191  uspgrn2crct  30194  crctcshwlkn0lem3  30198  crctcshwlkn0lem5  30200  wwlksnextbi  30280  wwlksnredwwlkn0  30282  wwlksnextinj  30285  wspthsnonn0vne  30303  umgr2adedgspth  30334  umgr2wlk  30335  usgr2wspthons3  30353  clwlkclwwlklem2a1  30380  clwlkclwwlklem2fv2  30384  clwlkclwwlklem2a4  30385  clwlkclwwlklem2a  30386  clwlkclwwlklem2  30388  clwwisshclwws  30403  erclwwlktr  30410  clwwlkn1loopb  30431  clwwlknwwlksnb  30443  clwwlkext2edg  30444  erclwwlkntr  30459  clwwlknon1  30485  clwwlknonwwlknonb  30494  clwwlknonex2lem2  30496  upgr1wlkdlem1  30533  upgr3v3e3cycl  30568  uhgr3cyclex  30570  upgr4cycl4dv4e  30573  eucrctshift  30631  frgr3vlem1  30661  3cyclfrgrrn1  30673  3cyclfrgrrn  30674  4cycl2vnunb  30678  frgrnbnb  30681  frgrncvvdeqlem8  30694  frgrwopreglem5  30709  frgrwopreglem5ALT  30710  frgr2wwlk1  30717  2clwwlk2clwwlk  30738  numclwwlk1lem2fo  30746  frgrreg  30782  friendshipgt3  30786  shmodsi  31778  kbass6  32510  mdsymlem6  32797  mdsymlem7  32798  cdj3lem2a  32825  cdj3lem3a  32828  satfrel  35879  gonarlem  35906  satffunlem1lem1  35914  satffunlem2lem1  35916  satffun  35921  wl-spae  38216  grpomndo  38566  rngoueqz  38631  zerdivemp1x  38638  elpcliN  40707  dflim5  44096  relexpiidm  44470  relexpxpmin  44483  ntrk0kbimka  44805  eel12131  45461  tratrbVD  45609  2uasbanhVD  45659  funressnfv  47820  funbrafv  47935  otiunsndisjX  48056  ssfz12  48091  iccpartgt  48216  iccelpart  48222  iccpartnel  48227  fargshiftf1  48230  sprsymrelfvlem  48279  sprsymrelf1lem  48280  prproropf1olem4  48295  sbcpr  48310  reupr  48311  poprelb  48313  reuopreuprim  48315  fmtno4prmfac  48364  lighneallem4b  48401  lighneal  48403  nprmdvdsfacm1lem2  48413  mogoldbblem  48525  gbegt5  48566  sbgoldbaltlem1  48584  sbgoldbm  48589  bgoldbtbndlem2  48611  bgoldbtbndlem3  48612  bgoldbtbndlem4  48613  bgoldbtbnd  48614  grimedg  48740  cycl3grtri  48752  grlimgrtri  48808  pgnbgreunbgrlem2lem1  48919  pgnbgreunbgrlem2lem2  48920  pgnbgreunbgrlem2lem3  48921  lidldomn1  49036  2zrngamgm  49050  rngccatidALTV  49077  ringccatidALTV  49111  scmsuppss  49191  ply1mulgsumlem1  49206  lincsumcl  49251  ellcoellss  49255  lindslinindsimp1  49277  lindslinindimp2lem1  49278  nn0sumshdiglemA  49439  nn0sumshdiglemB  49440  itschlc0xyqsol1  49586