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  1361  rspct  3551  po2nr  5546  wefrc  5618  tz7.7  6343  funssres  6536  isomin  7285  f1ocnv2d  7613  onint  7737  f1oweALT  7918  bropfvvvv  8035  tfrlem9  8317  tz7.49  8377  oelim  8462  oaordex  8486  omordi  8494  omass  8508  oen0  8515  nnmass  8553  nnmordi  8560  inf3lem2  9541  epfrs  9643  indcardi  9954  ackbij1lem16  10147  cfcoflem  10185  axcc3  10351  zorn2lem7  10415  grur1a  10733  genpcd  10920  genpnmax  10921  mulclprlem  10933  distrlem1pr  10939  ltaddpr  10948  ltexprlem6  10955  ltexprlem7  10956  mulgt0sr  11019  divgt0  12015  divge0  12016  sup2  12103  uzind2  12613  uzwo  12852  supxrun  13259  expnbnd  14185  facdiv  14240  hashimarni  14394  swrdswrdlem  14657  wrd2ind  14676  s3iunsndisj  14921  caubnd  15312  dvdsabseq  16273  lcmfunsnlem2lem1  16598  divgcdcoprm0  16625  ncoprmlnprm  16689  cshwshashlem1  17057  psgnunilem4  19463  lmodvsdi  20871  xrsdsreclblem  21402  nzerooringczr  21470  cpmatacl  22691  riinopn  22883  0ntr  23046  elcls  23048  hausnei2  23328  fgfil  23850  alexsubALTlem2  24023  alexsubALT  24026  aalioulem3  26311  aalioulem4  26312  wilthlem3  27047  2sqreultlem  27424  2sqreunnltlem  27427  bdayfinbndlem1  28473  finsumvtxdg2size  29634  upgrewlkle2  29690  upgrwlkdvdelem  29819  uhgrwkspthlem2  29837  clwwlkinwwlk  30125  wwlksext2clwwlk  30142  1pthon2v  30238  n4cyclfrgr  30376  frgrnbnb  30378  frgrwopreglem4a  30395  frgrreg  30479  frgrregord013  30480  grpoidinvlem3  30592  elspansn5  31660  atcv1  32466  atcvatlem  32471  chirredlem3  32478  mdsymlem3  32491  mdsymlem5  32493  mdsymlem6  32494  sumdmdlem2  32505  f1o3d  32714  slmdvsdi  33291  satfv0fun  35569  satffunlem1lem1  35600  satffunlem2lem1  35602  fgmin  36568  nndivsub  36655  mblfinlem3  37994  rngonegrmul  38279  crngm23  38337  hlrelat2  39863  pmaple  40221  pmodlem2  40307  dalaw  40346  sn-sup2  42950  syl5imp  44957  com3rgbi  44959  ee223  45079  relpmin  45397  2tceilhalfelfzo1  47796  iccpartigtl  47895  iccelpart  47905  lighneallem3  48082  bgoldbtbndlem3  48295  uhgrimisgrgric  48419  clnbgrgrim  48422  clnbgr3stgrgrlic  48508  gpgusgralem  48544  gpgvtxedg0  48551  gpgvtxedg1  48552  ply1mulgsumlem1  48874  fllog2  49056