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  1358  rspct  3546  po2nr  5519  wefrc  5585  tz7.7  6294  funssres  6480  isomin  7210  f1ocnv2d  7522  onint  7640  f1oweALT  7815  bropfvvvv  7930  wfrlem12OLD  8149  tfrlem9  8214  tz7.49  8274  oelim  8362  oaordex  8387  omordi  8395  omass  8409  oen0  8415  nnmass  8453  nnmordi  8460  inf3lem2  9385  epfrs  9487  indcardi  9795  ackbij1lem16  9989  cfcoflem  10026  axcc3  10192  zorn2lem7  10256  grur1a  10573  genpcd  10760  genpnmax  10761  mulclprlem  10773  distrlem1pr  10779  ltaddpr  10788  ltexprlem6  10795  ltexprlem7  10796  mulgt0sr  10859  divgt0  11841  divge0  11842  sup2  11929  uzind2  12411  uzwo  12649  supxrun  13048  expnbnd  13945  facdiv  13999  hashimarni  14154  swrdswrdlem  14415  wrd2ind  14434  s3iunsndisj  14677  caubnd  15068  dvdsabseq  16020  lcmfunsnlem2lem1  16341  divgcdcoprm0  16368  ncoprmlnprm  16430  cshwshashlem1  16795  psgnunilem4  19103  lmodvsdi  20144  xrsdsreclblem  20642  cpmatacl  21863  riinopn  22055  0ntr  22220  elcls  22222  hausnei2  22502  fgfil  23024  alexsubALTlem2  23197  alexsubALT  23200  aalioulem3  25492  aalioulem4  25493  wilthlem3  26217  2sqreultlem  26593  2sqreunnltlem  26596  finsumvtxdg2size  27915  upgrewlkle2  27971  upgrwlkdvdelem  28101  uhgrwkspthlem2  28119  clwwlkinwwlk  28401  wwlksext2clwwlk  28418  1pthon2v  28514  n4cyclfrgr  28652  frgrnbnb  28654  frgrwopreglem4a  28671  frgrreg  28755  frgrregord013  28756  grpoidinvlem3  28865  elspansn5  29933  atcv1  30739  atcvatlem  30744  chirredlem3  30751  mdsymlem3  30764  mdsymlem5  30766  mdsymlem6  30767  sumdmdlem2  30778  f1o3d  30959  slmdvsdi  31465  satfv0fun  33330  satffunlem1lem1  33361  satffunlem2lem1  33363  fgmin  34556  nndivsub  34643  mblfinlem3  35813  rngonegrmul  36099  crngm23  36157  hlrelat2  37414  pmaple  37772  pmodlem2  37858  dalaw  37897  sn-sup2  40436  syl5imp  42102  com3rgbi  42104  ee223  42224  iccpartigtl  44842  iccelpart  44852  lighneallem3  45026  bgoldbtbndlem3  45226  isomgrsym  45255  isomgrtr  45258  nzerooringczr  45597  ply1mulgsumlem1  45694  fllog2  45881