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  3607  po2nr  5610  wefrc  5682  tz7.7  6411  funssres  6611  isomin  7356  f1ocnv2d  7685  onint  7809  f1oweALT  7995  bropfvvvv  8115  wfrlem12OLD  8358  tfrlem9  8423  tz7.49  8483  oelim  8570  oaordex  8594  omordi  8602  omass  8616  oen0  8622  nnmass  8660  nnmordi  8667  inf3lem2  9666  epfrs  9768  indcardi  10078  ackbij1lem16  10271  cfcoflem  10309  axcc3  10475  zorn2lem7  10539  grur1a  10856  genpcd  11043  genpnmax  11044  mulclprlem  11056  distrlem1pr  11062  ltaddpr  11071  ltexprlem6  11078  ltexprlem7  11079  mulgt0sr  11142  divgt0  12133  divge0  12134  sup2  12221  uzind2  12708  uzwo  12950  supxrun  13354  expnbnd  14267  facdiv  14322  hashimarni  14476  swrdswrdlem  14738  wrd2ind  14757  s3iunsndisj  15003  caubnd  15393  dvdsabseq  16346  lcmfunsnlem2lem1  16671  divgcdcoprm0  16698  ncoprmlnprm  16761  cshwshashlem1  17129  psgnunilem4  19529  lmodvsdi  20899  xrsdsreclblem  21447  nzerooringczr  21508  cpmatacl  22737  riinopn  22929  0ntr  23094  elcls  23096  hausnei2  23376  fgfil  23898  alexsubALTlem2  24071  alexsubALT  24074  aalioulem3  26390  aalioulem4  26391  wilthlem3  27127  2sqreultlem  27505  2sqreunnltlem  27508  finsumvtxdg2size  29582  upgrewlkle2  29638  upgrwlkdvdelem  29768  uhgrwkspthlem2  29786  clwwlkinwwlk  30068  wwlksext2clwwlk  30085  1pthon2v  30181  n4cyclfrgr  30319  frgrnbnb  30321  frgrwopreglem4a  30338  frgrreg  30422  frgrregord013  30423  grpoidinvlem3  30534  elspansn5  31602  atcv1  32408  atcvatlem  32413  chirredlem3  32420  mdsymlem3  32433  mdsymlem5  32435  mdsymlem6  32436  sumdmdlem2  32447  f1o3d  32643  slmdvsdi  33203  satfv0fun  35355  satffunlem1lem1  35386  satffunlem2lem1  35388  fgmin  36352  nndivsub  36439  mblfinlem3  37645  rngonegrmul  37930  crngm23  37988  hlrelat2  39385  pmaple  39743  pmodlem2  39829  dalaw  39868  sn-sup2  42477  syl5imp  44509  com3rgbi  44511  ee223  44631  iccpartigtl  47347  iccelpart  47357  lighneallem3  47531  bgoldbtbndlem3  47731  uhgrimisgrgric  47836  clnbgrgrim  47839  clnbgr3stgrgrlic  47914  gpgusgralem  47945  2tceilhalfelfzo1  47952  gpgvtxedg0  47955  gpgvtxedg1  47956  ply1mulgsumlem1  48231  fllog2  48417