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  1359  rspct  3568  po2nr  5564  wefrc  5632  tz7.7  6348  funssres  6550  isomin  7287  f1ocnv2d  7611  onint  7730  f1oweALT  7910  bropfvvvv  8029  wfrlem12OLD  8271  tfrlem9  8336  tz7.49  8396  oelim  8485  oaordex  8510  omordi  8518  omass  8532  oen0  8538  nnmass  8576  nnmordi  8583  inf3lem2  9574  epfrs  9676  indcardi  9986  ackbij1lem16  10180  cfcoflem  10217  axcc3  10383  zorn2lem7  10447  grur1a  10764  genpcd  10951  genpnmax  10952  mulclprlem  10964  distrlem1pr  10970  ltaddpr  10979  ltexprlem6  10986  ltexprlem7  10987  mulgt0sr  11050  divgt0  12032  divge0  12033  sup2  12120  uzind2  12605  uzwo  12845  supxrun  13245  expnbnd  14145  facdiv  14197  hashimarni  14351  swrdswrdlem  14604  wrd2ind  14623  s3iunsndisj  14865  caubnd  15255  dvdsabseq  16206  lcmfunsnlem2lem1  16525  divgcdcoprm0  16552  ncoprmlnprm  16614  cshwshashlem1  16979  psgnunilem4  19293  lmodvsdi  20402  xrsdsreclblem  20880  cpmatacl  22102  riinopn  22294  0ntr  22459  elcls  22461  hausnei2  22741  fgfil  23263  alexsubALTlem2  23436  alexsubALT  23439  aalioulem3  25731  aalioulem4  25732  wilthlem3  26456  2sqreultlem  26832  2sqreunnltlem  26835  finsumvtxdg2size  28561  upgrewlkle2  28617  upgrwlkdvdelem  28747  uhgrwkspthlem2  28765  clwwlkinwwlk  29047  wwlksext2clwwlk  29064  1pthon2v  29160  n4cyclfrgr  29298  frgrnbnb  29300  frgrwopreglem4a  29317  frgrreg  29401  frgrregord013  29402  grpoidinvlem3  29511  elspansn5  30579  atcv1  31385  atcvatlem  31390  chirredlem3  31397  mdsymlem3  31410  mdsymlem5  31412  mdsymlem6  31413  sumdmdlem2  31424  f1o3d  31608  slmdvsdi  32120  satfv0fun  34052  satffunlem1lem1  34083  satffunlem2lem1  34085  fgmin  34918  nndivsub  35005  mblfinlem3  36190  rngonegrmul  36476  crngm23  36534  hlrelat2  37939  pmaple  38297  pmodlem2  38383  dalaw  38422  sn-sup2  40996  syl5imp  42916  com3rgbi  42918  ee223  43038  iccpartigtl  45735  iccelpart  45745  lighneallem3  45919  bgoldbtbndlem3  46119  isomgrsym  46148  isomgrtr  46151  nzerooringczr  46490  ply1mulgsumlem1  46587  fllog2  46774