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  1357  rspct  3537  po2nr  5508  wefrc  5574  tz7.7  6277  funssres  6462  isomin  7188  f1ocnv2d  7500  onint  7617  f1oweALT  7788  bropfvvvv  7903  wfrlem12OLD  8122  tfrlem9  8187  tz7.49  8246  oelim  8326  oaordex  8351  omordi  8359  omass  8373  oen0  8379  nnmass  8417  nnmordi  8424  inf3lem2  9317  epfrs  9420  indcardi  9728  ackbij1lem16  9922  cfcoflem  9959  axcc3  10125  zorn2lem7  10189  grur1a  10506  genpcd  10693  genpnmax  10694  mulclprlem  10706  distrlem1pr  10712  ltaddpr  10721  ltexprlem6  10728  ltexprlem7  10729  mulgt0sr  10792  divgt0  11773  divge0  11774  sup2  11861  uzind2  12343  uzwo  12580  supxrun  12979  expnbnd  13875  facdiv  13929  hashimarni  14084  swrdswrdlem  14345  wrd2ind  14364  s3iunsndisj  14607  caubnd  14998  dvdsabseq  15950  lcmfunsnlem2lem1  16271  divgcdcoprm0  16298  ncoprmlnprm  16360  cshwshashlem1  16725  psgnunilem4  19020  lmodvsdi  20061  xrsdsreclblem  20556  cpmatacl  21773  riinopn  21965  0ntr  22130  elcls  22132  hausnei2  22412  fgfil  22934  alexsubALTlem2  23107  alexsubALT  23110  aalioulem3  25399  aalioulem4  25400  wilthlem3  26124  2sqreultlem  26500  2sqreunnltlem  26503  finsumvtxdg2size  27820  upgrewlkle2  27876  upgrwlkdvdelem  28005  uhgrwkspthlem2  28023  clwwlkinwwlk  28305  wwlksext2clwwlk  28322  1pthon2v  28418  n4cyclfrgr  28556  frgrnbnb  28558  frgrwopreglem4a  28575  frgrreg  28659  frgrregord013  28660  grpoidinvlem3  28769  elspansn5  29837  atcv1  30643  atcvatlem  30648  chirredlem3  30655  mdsymlem3  30668  mdsymlem5  30670  mdsymlem6  30671  sumdmdlem2  30682  f1o3d  30863  slmdvsdi  31370  satfv0fun  33233  satffunlem1lem1  33264  satffunlem2lem1  33266  fgmin  34486  nndivsub  34573  mblfinlem3  35743  rngonegrmul  36029  crngm23  36087  hlrelat2  37344  pmaple  37702  pmodlem2  37788  dalaw  37827  sn-sup2  40360  syl5imp  42021  com3rgbi  42023  ee223  42143  iccpartigtl  44763  iccelpart  44773  lighneallem3  44947  bgoldbtbndlem3  45147  isomgrsym  45176  isomgrtr  45179  nzerooringczr  45518  ply1mulgsumlem1  45615  fllog2  45802