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  1360  rspct  3577  po2nr  5563  wefrc  5635  tz7.7  6361  funssres  6563  isomin  7315  f1ocnv2d  7645  onint  7769  f1oweALT  7954  bropfvvvv  8074  tfrlem9  8356  tz7.49  8416  oelim  8501  oaordex  8525  omordi  8533  omass  8547  oen0  8553  nnmass  8591  nnmordi  8598  inf3lem2  9589  epfrs  9691  indcardi  10001  ackbij1lem16  10194  cfcoflem  10232  axcc3  10398  zorn2lem7  10462  grur1a  10779  genpcd  10966  genpnmax  10967  mulclprlem  10979  distrlem1pr  10985  ltaddpr  10994  ltexprlem6  11001  ltexprlem7  11002  mulgt0sr  11065  divgt0  12058  divge0  12059  sup2  12146  uzind2  12634  uzwo  12877  supxrun  13283  expnbnd  14204  facdiv  14259  hashimarni  14413  swrdswrdlem  14676  wrd2ind  14695  s3iunsndisj  14941  caubnd  15332  dvdsabseq  16290  lcmfunsnlem2lem1  16615  divgcdcoprm0  16642  ncoprmlnprm  16705  cshwshashlem1  17073  psgnunilem4  19434  lmodvsdi  20798  xrsdsreclblem  21336  nzerooringczr  21397  cpmatacl  22610  riinopn  22802  0ntr  22965  elcls  22967  hausnei2  23247  fgfil  23769  alexsubALTlem2  23942  alexsubALT  23945  aalioulem3  26249  aalioulem4  26250  wilthlem3  26987  2sqreultlem  27365  2sqreunnltlem  27368  finsumvtxdg2size  29485  upgrewlkle2  29541  upgrwlkdvdelem  29673  uhgrwkspthlem2  29691  clwwlkinwwlk  29976  wwlksext2clwwlk  29993  1pthon2v  30089  n4cyclfrgr  30227  frgrnbnb  30229  frgrwopreglem4a  30246  frgrreg  30330  frgrregord013  30331  grpoidinvlem3  30442  elspansn5  31510  atcv1  32316  atcvatlem  32321  chirredlem3  32328  mdsymlem3  32341  mdsymlem5  32343  mdsymlem6  32344  sumdmdlem2  32355  f1o3d  32558  slmdvsdi  33175  satfv0fun  35365  satffunlem1lem1  35396  satffunlem2lem1  35398  fgmin  36365  nndivsub  36452  mblfinlem3  37660  rngonegrmul  37945  crngm23  38003  hlrelat2  39404  pmaple  39762  pmodlem2  39848  dalaw  39887  sn-sup2  42486  syl5imp  44509  com3rgbi  44511  ee223  44631  relpmin  44949  2tceilhalfelfzo1  47337  iccpartigtl  47428  iccelpart  47438  lighneallem3  47612  bgoldbtbndlem3  47812  uhgrimisgrgric  47935  clnbgrgrim  47938  clnbgr3stgrgrlic  48015  gpgusgralem  48051  gpgvtxedg0  48058  gpgvtxedg1  48059  ply1mulgsumlem1  48379  fllog2  48561