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  ad5ant14OLD  1218  ad5ant15OLD  1220  ad5ant24OLD  1224  ad5ant25OLD  1226  3an1rsOLD  1438  3an1rs  1452  ad5ant124OLD  1463  ad5ant134OLD  1467  ad5ant135OLD  1469  rspct  3453  po2nr  5183  wefrc  5243  tz7.7  5892  funssres  6073  isomin  6730  f1ocnv2d  7033  onint  7142  f1oweALT  7299  bropfvvvv  7408  wfrlem12  7579  tfrlem9  7634  tz7.49  7693  oelim  7768  oaordex  7792  omordi  7800  omass  7814  oen0  7820  nnmass  7858  nnmordi  7865  inf3lem2  8690  epfrs  8771  indcardi  9064  ackbij1lem16  9259  cfcoflem  9296  axcc3  9462  zorn2lem7  9526  grur1a  9843  genpcd  10030  genpnmax  10031  mulclprlem  10043  distrlem1pr  10049  ltaddpr  10058  ltexprlem6  10065  ltexprlem7  10066  mulgt0sr  10128  divgt0  11093  divge0  11094  sup2  11181  uzind2  11672  uzwo  11954  supxrun  12351  expnbnd  13200  facdiv  13278  hashimarni  13430  swrdswrdlem  13668  wrd2ind  13686  s3iunsndisj  13917  caubnd  14306  dvdsabseq  15244  lcmfunsnlem2lem1  15559  divgcdcoprm0  15586  ncoprmlnprm  15643  cshwshashlem1  16009  psgnunilem4  18124  lmodvsdi  19096  xrsdsreclblem  20007  cpmatacl  20741  riinopn  20933  0ntr  21096  elcls  21098  hausnei2  21378  fgfil  21899  alexsubALTlem2  22072  alexsubALT  22075  aalioulem3  24309  aalioulem4  24310  wilthlem3  25017  finsumvtxdg2size  26681  upgrewlkle2  26737  upgrwlkdvdelem  26867  uhgrwkspthlem2  26885  clwwlkinwwlk  27196  wwlksext2clwwlk  27214  1pthon2v  27333  n4cyclfrgr  27473  frgrnbnb  27475  frgrwopreglem4a  27492  frgrreg  27593  frgrregord013  27594  grpoidinvlem3  27700  elspansn5  28773  atcv1  29579  atcvatlem  29584  chirredlem3  29591  mdsymlem3  29604  mdsymlem5  29606  mdsymlem6  29607  sumdmdlem2  29618  f1o3d  29771  slmdvsdi  30108  fgmin  32702  nndivsub  32793  mblfinlem3  33781  rngonegrmul  34075  crngm23  34133  hlrelat2  35211  pmaple  35569  pmodlem2  35655  dalaw  35694  syl5imp  39243  com3rgbi  39245  ee223  39384  iccpartigtl  41887  iccelpart  41897  lighneallem3  42052  bgoldbtbndlem3  42223  nzerooringczr  42600  ply1mulgsumlem1  42702  fllog2  42890