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  3547  po2nr  5517  wefrc  5583  tz7.7  6292  funssres  6478  isomin  7208  f1ocnv2d  7522  onint  7640  f1oweALT  7815  bropfvvvv  7932  wfrlem12OLD  8151  tfrlem9  8216  tz7.49  8276  oelim  8364  oaordex  8389  omordi  8397  omass  8411  oen0  8417  nnmass  8455  nnmordi  8462  inf3lem2  9387  epfrs  9489  indcardi  9797  ackbij1lem16  9991  cfcoflem  10028  axcc3  10194  zorn2lem7  10258  grur1a  10575  genpcd  10762  genpnmax  10763  mulclprlem  10775  distrlem1pr  10781  ltaddpr  10790  ltexprlem6  10797  ltexprlem7  10798  mulgt0sr  10861  divgt0  11843  divge0  11844  sup2  11931  uzind2  12413  uzwo  12651  supxrun  13050  expnbnd  13947  facdiv  14001  hashimarni  14156  swrdswrdlem  14417  wrd2ind  14436  s3iunsndisj  14679  caubnd  15070  dvdsabseq  16022  lcmfunsnlem2lem1  16343  divgcdcoprm0  16370  ncoprmlnprm  16432  cshwshashlem1  16797  psgnunilem4  19105  lmodvsdi  20146  xrsdsreclblem  20644  cpmatacl  21865  riinopn  22057  0ntr  22222  elcls  22224  hausnei2  22504  fgfil  23026  alexsubALTlem2  23199  alexsubALT  23202  aalioulem3  25494  aalioulem4  25495  wilthlem3  26219  2sqreultlem  26595  2sqreunnltlem  26598  finsumvtxdg2size  27917  upgrewlkle2  27973  upgrwlkdvdelem  28104  uhgrwkspthlem2  28122  clwwlkinwwlk  28404  wwlksext2clwwlk  28421  1pthon2v  28517  n4cyclfrgr  28655  frgrnbnb  28657  frgrwopreglem4a  28674  frgrreg  28758  frgrregord013  28759  grpoidinvlem3  28868  elspansn5  29936  atcv1  30742  atcvatlem  30747  chirredlem3  30754  mdsymlem3  30767  mdsymlem5  30769  mdsymlem6  30770  sumdmdlem2  30781  f1o3d  30962  slmdvsdi  31468  satfv0fun  33333  satffunlem1lem1  33364  satffunlem2lem1  33366  fgmin  34559  nndivsub  34646  mblfinlem3  35816  rngonegrmul  36102  crngm23  36160  hlrelat2  37417  pmaple  37775  pmodlem2  37861  dalaw  37900  sn-sup2  40439  syl5imp  42132  com3rgbi  42134  ee223  42254  iccpartigtl  44875  iccelpart  44885  lighneallem3  45059  bgoldbtbndlem3  45259  isomgrsym  45288  isomgrtr  45291  nzerooringczr  45630  ply1mulgsumlem1  45727  fllog2  45914