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  3599  po2nr  5603  wefrc  5671  tz7.7  6391  funssres  6593  isomin  7334  f1ocnv2d  7659  onint  7778  f1oweALT  7959  bropfvvvv  8078  wfrlem12OLD  8320  tfrlem9  8385  tz7.49  8445  oelim  8534  oaordex  8558  omordi  8566  omass  8580  oen0  8586  nnmass  8624  nnmordi  8631  inf3lem2  9624  epfrs  9726  indcardi  10036  ackbij1lem16  10230  cfcoflem  10267  axcc3  10433  zorn2lem7  10497  grur1a  10814  genpcd  11001  genpnmax  11002  mulclprlem  11014  distrlem1pr  11020  ltaddpr  11029  ltexprlem6  11036  ltexprlem7  11037  mulgt0sr  11100  divgt0  12082  divge0  12083  sup2  12170  uzind2  12655  uzwo  12895  supxrun  13295  expnbnd  14195  facdiv  14247  hashimarni  14401  swrdswrdlem  14654  wrd2ind  14673  s3iunsndisj  14915  caubnd  15305  dvdsabseq  16256  lcmfunsnlem2lem1  16575  divgcdcoprm0  16602  ncoprmlnprm  16664  cshwshashlem1  17029  psgnunilem4  19365  lmodvsdi  20495  xrsdsreclblem  20991  cpmatacl  22218  riinopn  22410  0ntr  22575  elcls  22577  hausnei2  22857  fgfil  23379  alexsubALTlem2  23552  alexsubALT  23555  aalioulem3  25847  aalioulem4  25848  wilthlem3  26574  2sqreultlem  26950  2sqreunnltlem  26953  finsumvtxdg2size  28807  upgrewlkle2  28863  upgrwlkdvdelem  28993  uhgrwkspthlem2  29011  clwwlkinwwlk  29293  wwlksext2clwwlk  29310  1pthon2v  29406  n4cyclfrgr  29544  frgrnbnb  29546  frgrwopreglem4a  29563  frgrreg  29647  frgrregord013  29648  grpoidinvlem3  29759  elspansn5  30827  atcv1  31633  atcvatlem  31638  chirredlem3  31645  mdsymlem3  31658  mdsymlem5  31660  mdsymlem6  31661  sumdmdlem2  31672  f1o3d  31851  slmdvsdi  32360  satfv0fun  34362  satffunlem1lem1  34393  satffunlem2lem1  34395  fgmin  35255  nndivsub  35342  mblfinlem3  36527  rngonegrmul  36812  crngm23  36870  hlrelat2  38274  pmaple  38632  pmodlem2  38718  dalaw  38757  sn-sup2  41342  syl5imp  43273  com3rgbi  43275  ee223  43395  iccpartigtl  46091  iccelpart  46101  lighneallem3  46275  bgoldbtbndlem3  46475  isomgrsym  46504  isomgrtr  46507  nzerooringczr  46970  ply1mulgsumlem1  47067  fllog2  47254