Theorem com34 91

Description: Commutation of antecedents. Swap 3rd and 4th. Deduction associated with com23 86. Double deduction associated with com12 32. (Contributed by NM, 25-Apr-1994.)

Hypothesis

Ref	Expression
com4.1	⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

Assertion

Ref	Expression
com34	⊢ (𝜑 → (𝜓 → (𝜃 → (𝜒 → 𝜏))))

Proof of Theorem com34

Step	Hyp	Ref	Expression
1		com4.1	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
2		pm2.04 90	. 2 ⊢ ((𝜒 → (𝜃 → 𝜏)) → (𝜃 → (𝜒 → 𝜏)))
3	1, 2	syl6 35	1 ⊢ (𝜑 → (𝜓 → (𝜃 → (𝜒 → 𝜏))))

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  com4l  92  com35  98  3an1rs  1360  rspct  3608  po2nr  5606  wefrc  5679  tz7.7  6410  funssres  6610  isomin  7357  f1ocnv2d  7686  onint  7810  f1oweALT  7997  bropfvvvv  8117  wfrlem12OLD  8360  tfrlem9  8425  tz7.49  8485  oelim  8572  oaordex  8596  omordi  8604  omass  8618  oen0  8624  nnmass  8662  nnmordi  8669  inf3lem2  9669  epfrs  9771  indcardi  10081  ackbij1lem16  10274  cfcoflem  10312  axcc3  10478  zorn2lem7  10542  grur1a  10859  genpcd  11046  genpnmax  11047  mulclprlem  11059  distrlem1pr  11065  ltaddpr  11074  ltexprlem6  11081  ltexprlem7  11082  mulgt0sr  11145  divgt0  12136  divge0  12137  sup2  12224  uzind2  12711  uzwo  12953  supxrun  13358  expnbnd  14271  facdiv  14326  hashimarni  14480  swrdswrdlem  14742  wrd2ind  14761  s3iunsndisj  15007  caubnd  15397  dvdsabseq  16350  lcmfunsnlem2lem1  16675  divgcdcoprm0  16702  ncoprmlnprm  16765  cshwshashlem1  17133  psgnunilem4  19515  lmodvsdi  20883  xrsdsreclblem  21430  nzerooringczr  21491  cpmatacl  22722  riinopn  22914  0ntr  23079  elcls  23081  hausnei2  23361  fgfil  23883  alexsubALTlem2  24056  alexsubALT  24059  aalioulem3  26376  aalioulem4  26377  wilthlem3  27113  2sqreultlem  27491  2sqreunnltlem  27494  finsumvtxdg2size  29568  upgrewlkle2  29624  upgrwlkdvdelem  29756  uhgrwkspthlem2  29774  clwwlkinwwlk  30059  wwlksext2clwwlk  30076  1pthon2v  30172  n4cyclfrgr  30310  frgrnbnb  30312  frgrwopreglem4a  30329  frgrreg  30413  frgrregord013  30414  grpoidinvlem3  30525  elspansn5  31593  atcv1  32399  atcvatlem  32404  chirredlem3  32411  mdsymlem3  32424  mdsymlem5  32426  mdsymlem6  32427  sumdmdlem2  32438  f1o3d  32637  slmdvsdi  33221  satfv0fun  35376  satffunlem1lem1  35407  satffunlem2lem1  35409  fgmin  36371  nndivsub  36458  mblfinlem3  37666  rngonegrmul  37951  crngm23  38009  hlrelat2  39405  pmaple  39763  pmodlem2  39849  dalaw  39888  sn-sup2  42501  syl5imp  44532  com3rgbi  44534  ee223  44654  relpmin  44973  iccpartigtl  47410  iccelpart  47420  lighneallem3  47594  bgoldbtbndlem3  47794  uhgrimisgrgric  47899  clnbgrgrim  47902  clnbgr3stgrgrlic  47979  gpgusgralem  48011  2tceilhalfelfzo1  48018  gpgvtxedg0  48021  gpgvtxedg1  48022  ply1mulgsumlem1  48303  fllog2  48489