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  1355  rspct  3609  po2nr  5487  wefrc  5549  tz7.7  6217  funssres  6398  isomin  7090  f1ocnv2d  7398  onint  7510  f1oweALT  7673  bropfvvvv  7787  wfrlem12  7966  tfrlem9  8021  tz7.49  8081  oelim  8159  oaordex  8184  omordi  8192  omass  8206  oen0  8212  nnmass  8250  nnmordi  8257  inf3lem2  9092  epfrs  9173  indcardi  9467  ackbij1lem16  9657  cfcoflem  9694  axcc3  9860  zorn2lem7  9924  grur1a  10241  genpcd  10428  genpnmax  10429  mulclprlem  10441  distrlem1pr  10447  ltaddpr  10456  ltexprlem6  10463  ltexprlem7  10464  mulgt0sr  10527  divgt0  11508  divge0  11509  sup2  11597  uzind2  12076  uzwo  12312  supxrun  12710  expnbnd  13594  facdiv  13648  hashimarni  13803  swrdswrdlem  14066  wrd2ind  14085  s3iunsndisj  14328  caubnd  14718  dvdsabseq  15663  lcmfunsnlem2lem1  15982  divgcdcoprm0  16009  ncoprmlnprm  16068  cshwshashlem1  16429  psgnunilem4  18625  lmodvsdi  19657  xrsdsreclblem  20591  cpmatacl  21324  riinopn  21516  0ntr  21679  elcls  21681  hausnei2  21961  fgfil  22483  alexsubALTlem2  22656  alexsubALT  22659  aalioulem3  24923  aalioulem4  24924  wilthlem3  25647  2sqreultlem  26023  2sqreunnltlem  26026  finsumvtxdg2size  27332  upgrewlkle2  27388  upgrwlkdvdelem  27517  uhgrwkspthlem2  27535  clwwlkinwwlk  27818  wwlksext2clwwlk  27836  1pthon2v  27932  n4cyclfrgr  28070  frgrnbnb  28072  frgrwopreglem4a  28089  frgrreg  28173  frgrregord013  28174  grpoidinvlem3  28283  elspansn5  29351  atcv1  30157  atcvatlem  30162  chirredlem3  30169  mdsymlem3  30182  mdsymlem5  30184  mdsymlem6  30185  sumdmdlem2  30196  f1o3d  30372  slmdvsdi  30843  satfv0fun  32618  satffunlem1lem1  32649  satffunlem2lem1  32651  fgmin  33718  nndivsub  33805  mblfinlem3  34946  rngonegrmul  35237  crngm23  35295  hlrelat2  36554  pmaple  36912  pmodlem2  36998  dalaw  37037  syl5imp  40895  com3rgbi  40897  ee223  41017  iccpartigtl  43632  iccelpart  43642  lighneallem3  43821  bgoldbtbndlem3  44021  isomgrsym  44050  isomgrtr  44053  nzerooringczr  44392  ply1mulgsumlem1  44489  fllog2  44677