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  4819  3elpr2eq  4866  propeqop  5479  po2ne  5575  funopg  6566  eldmrexrnb  7084  peano5  7894  f1o2ndf1  8122  suppimacnv  8175  omordi  8558  omeulem1  8574  brecop  8815  isinf  9240  fiint  9302  carduni  10043  dfac5  10188  dfac2b  10190  cofsmo  10328  cfcoflem  10331  domtriomlem  10501  axdc3lem2  10510  nqereu  10995  squeeze0  12201  zmax  13053  elpq  13084  xnn0lenn0nn0  13356  xrsupsslem  13418  xrinfmsslem  13419  supxrunb1  13430  supxrunb2  13431  difreicc  13596  elfz0ubfz0  13746  elfz0fzfz0  13747  fz0fzelfz0  13748  fz0fzdiffz0  13751  fzo1fzo0n0  13830  elfzodifsumelfzo  13846  ssfzo12  13874  ssfzo12bi  13876  fzoopth  13877  elfznelfzo  13888  injresinjlem  13905  injresinj  13906  addmodlteq  14069  uzindi  14105  ssnn0fi  14108  suppssfz  14117  facwordi  14413  hasheqf1oi  14475  hashf1rn  14476  fundmge2nop0  14627  swrdswrdlem  14833  swrdswrd  14834  wrd2ind  14852  swrdccatin1  14854  pfxccatin12lem2  14860  swrdccat  14864  reuccatpfxs1lem  14875  repsdf2  14909  cshwidx0  14937  cshweqrep  14952  2cshwcshw  14956  cshwcsh2id  14959  swrdco  14968  wwlktovfo  15091  sqrt2irr  16397  oddnn02np1  16498  oddge22np1  16499  evennn02n  16500  evennn2n  16501  dfgcd2  16699  lcmf  16788  lcmfunsnlem2lem2  16794  initoeu2lem1  18169  symgfix2  19610  gsmsymgreqlem2  19625  psgnunilem4  19691  01eq0ringOLD  20762  lmodfopnelem1  21153  nzerooringczr  21766  cply1mul  22594  gsummoncoe1  22606  mamufacex  22691  matecl  22720  gsummatr01  22954  mp2pm2mplem4  23107  chfacfscmul0  23156  chfacfpmmul0  23160  cayhamlem1  23164  fbunfip  24168  tngngp3  24955  mpomulcn  25168  zabsle1  27605  gausslemma2dlem1a  27674  2lgsoddprm  27725  2sqreunnltblem  27760  fltoprmlem2  27976  umgrnloopv  29666  upgredg2vtx  29701  usgruspgrb  29746  usgrnloopvALT  29764  usgredg2vlem2  29789  edg0usgr  29816  nbuhgr  29906  nbumgr  29910  nbuhgr2vtx1edgblem  29914  cusgredg  29987  cusgrsize2inds  30016  sizusglecusg  30026  umgr2v2enb1  30089  rusgr1vtx  30151  uspgr2wlkeq  30208  wlkreslem  30230  spthonepeq  30320  usgr2trlspth  30329  clwlkl1loop  30352  lfgrn1cycl  30376  uspgrn2crct  30379  crctcshwlkn0lem3  30383  crctcshwlkn0lem5  30385  wwlksnextbi  30465  wwlksnredwwlkn0  30467  wwlksnextinj  30470  wspthsnonn0vne  30488  umgr2adedgspth  30519  umgr2wlk  30520  usgr2wspthons3  30538  clwlkclwwlklem2a1  30565  clwlkclwwlklem2fv2  30569  clwlkclwwlklem2a4  30570  clwlkclwwlklem2a  30571  clwlkclwwlklem2  30573  clwwisshclwws  30588  erclwwlktr  30595  clwwlkn1loopb  30616  clwwlknwwlksnb  30628  clwwlkext2edg  30629  erclwwlkntr  30644  clwwlknon1  30670  clwwlknonwwlknonb  30679  clwwlknonex2lem2  30681  upgr1wlkdlem1  30718  upgr3v3e3cycl  30763  uhgr3cyclex  30765  upgr4cycl4dv4e  30768  eucrctshift  30826  frgr3vlem1  30856  3cyclfrgrrn1  30868  3cyclfrgrrn  30869  4cycl2vnunb  30873  frgrnbnb  30876  frgrncvvdeqlem8  30889  frgrwopreglem5  30904  frgrwopreglem5ALT  30905  frgr2wwlk1  30912  2clwwlk2clwwlk  30933  numclwwlk1lem2fo  30941  frgrreg  30977  friendshipgt3  30981  shmodsi  31973  kbass6  32705  mdsymlem6  32992  mdsymlem7  32993  cdj3lem2a  33020  cdj3lem3a  33023  satfrel  36101  gonarlem  36128  satffunlem1lem1  36136  satffunlem2lem1  36138  satffun  36143  wl-spae  38421  grpomndo  38777  rngoueqz  38842  zerdivemp1x  38849  elpcliN  40918  dflim5  44289  relexpiidm  44663  relexpxpmin  44676  ntrk0kbimka  44998  eel12131  45654  tratrbVD  45802  2uasbanhVD  45852  funressnfv  48057  funbrafv  48172  otiunsndisjX  48293  ssfz12  48328  iccpartgt  48453  iccelpart  48459  iccpartnel  48464  fargshiftf1  48467  sprsymrelfvlem  48516  sprsymrelf1lem  48517  prproropf1olem4  48532  sbcpr  48547  reupr  48548  poprelb  48550  reuopreuprim  48552  fmtno4prmfac  48601  lighneallem4b  48638  lighneal  48640  nprmdvdsfacm1lem2  48650  mogoldbblem  48762  gbegt5  48803  sbgoldbaltlem1  48821  sbgoldbm  48826  bgoldbtbndlem2  48848  bgoldbtbndlem3  48849  bgoldbtbndlem4  48850  bgoldbtbnd  48851  grimedg  48977  cycl3grtri  48989  grlimgrtri  49045  pgnbgreunbgrlem2lem1  49156  pgnbgreunbgrlem2lem2  49157  pgnbgreunbgrlem2lem3  49158  lidldomn1  49272  2zrngamgm  49286  rngccatidALTV  49313  ringccatidALTV  49347  scmsuppss  49427  ply1mulgsumlem1  49442  lincsumcl  49487  ellcoellss  49491  lindslinindsimp1  49513  lindslinindimp2lem1  49514  nn0sumshdiglemA  49675  nn0sumshdiglemB  49676  itschlc0xyqsol1  49822