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  1372  rspct  3566  po2nr  5565  wefrc  5637  tz7.7  6366  funssres  6559  isomin  7315  f1ocnv2d  7643  onint  7767  f1oweALT  7947  bropfvvvv  8064  tfrlem9  8349  tz7.49  8409  oelim  8496  oaordex  8520  omordi  8528  omass  8542  oen0  8549  nnmass  8587  nnmordi  8594  inf3lem2  9577  epfrs  9679  indcardi  9990  ackbij1lem16  10183  cfcoflem  10222  axcc3  10388  zorn2lem7  10452  grur1a  10770  genpcd  10957  genpnmax  10958  mulclprlem  10970  distrlem1pr  10976  ltaddpr  10985  ltexprlem6  10992  ltexprlem7  10993  mulgt0sr  11056  divgt0  12053  divge0  12054  sup2  12141  uzind2  12659  uzwo  12905  supxrun  13312  expnbnd  14238  facdiv  14293  hashimarni  14447  swrdswrdlem  14710  wrd2ind  14729  s3iunsndisj  14974  caubnd  15376  dvdsabseq  16337  lcmfunsnlem2lem1  16662  divgcdcoprm0  16689  ncoprmlnprm  16753  cshwshashlem1  17121  psgnunilem4  19527  lmodvsdi  20939  xrsdsreclblem  21452  nzerooringczr  21519  cpmatacl  22763  riinopn  22955  0ntr  23118  elcls  23120  hausnei2  23400  fgfil  23922  alexsubALTlem2  24095  alexsubALT  24098  aalioulem3  26385  aalioulem4  26386  wilthlem3  27121  2sqreultlem  27498  2sqreunnltlem  27501  bdayfinbndlem1  28547  finsumvtxdg2size  29707  upgrewlkle2  29763  upgrwlkdvdelem  29892  uhgrwkspthlem2  29910  clwwlkinwwlk  30198  wwlksext2clwwlk  30215  1pthon2v  30311  n4cyclfrgr  30449  frgrnbnb  30451  frgrwopreglem4a  30468  frgrreg  30552  frgrregord013  30553  grpoidinvlem3  30665  elspansn5  31733  atcv1  32539  atcvatlem  32544  chirredlem3  32551  mdsymlem3  32564  mdsymlem5  32566  mdsymlem6  32567  sumdmdlem2  32578  f1o3d  32788  slmdvsdi  33355  satfv0fun  35681  satffunlem1lem1  35712  satffunlem2lem1  35714  fgmin  36690  nndivsub  36777  mblfinlem3  38118  rngonegrmul  38403  crngm23  38461  hlrelat2  39987  pmaple  40345  pmodlem2  40431  dalaw  40470  sn-sup2  43073  syl5imp  45048  com3rgbi  45050  ee223  45170  relpmin  45488  2tceilhalfelfzo1  47890  iccpartigtl  47989  iccelpart  47999  lighneallem3  48176  bgoldbtbndlem3  48389  uhgrimisgrgric  48513  clnbgrgrim  48516  clnbgr3stgrgrlic  48602  gpgusgralem  48638  gpgvtxedg0  48645  gpgvtxedg1  48646  ply1mulgsumlem1  48968  fllog2  49150