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  3574  po2nr  5560  wefrc  5632  tz7.7  6358  funssres  6560  isomin  7312  f1ocnv2d  7642  onint  7766  f1oweALT  7951  bropfvvvv  8071  tfrlem9  8353  tz7.49  8413  oelim  8498  oaordex  8522  omordi  8530  omass  8544  oen0  8550  nnmass  8588  nnmordi  8595  inf3lem2  9582  epfrs  9684  indcardi  9994  ackbij1lem16  10187  cfcoflem  10225  axcc3  10391  zorn2lem7  10455  grur1a  10772  genpcd  10959  genpnmax  10960  mulclprlem  10972  distrlem1pr  10978  ltaddpr  10987  ltexprlem6  10994  ltexprlem7  10995  mulgt0sr  11058  divgt0  12051  divge0  12052  sup2  12139  uzind2  12627  uzwo  12870  supxrun  13276  expnbnd  14197  facdiv  14252  hashimarni  14406  swrdswrdlem  14669  wrd2ind  14688  s3iunsndisj  14934  caubnd  15325  dvdsabseq  16283  lcmfunsnlem2lem1  16608  divgcdcoprm0  16635  ncoprmlnprm  16698  cshwshashlem1  17066  psgnunilem4  19427  lmodvsdi  20791  xrsdsreclblem  21329  nzerooringczr  21390  cpmatacl  22603  riinopn  22795  0ntr  22958  elcls  22960  hausnei2  23240  fgfil  23762  alexsubALTlem2  23935  alexsubALT  23938  aalioulem3  26242  aalioulem4  26243  wilthlem3  26980  2sqreultlem  27358  2sqreunnltlem  27361  finsumvtxdg2size  29478  upgrewlkle2  29534  upgrwlkdvdelem  29666  uhgrwkspthlem2  29684  clwwlkinwwlk  29969  wwlksext2clwwlk  29986  1pthon2v  30082  n4cyclfrgr  30220  frgrnbnb  30222  frgrwopreglem4a  30239  frgrreg  30323  frgrregord013  30324  grpoidinvlem3  30435  elspansn5  31503  atcv1  32309  atcvatlem  32314  chirredlem3  32321  mdsymlem3  32334  mdsymlem5  32336  mdsymlem6  32337  sumdmdlem2  32348  f1o3d  32551  slmdvsdi  33168  satfv0fun  35358  satffunlem1lem1  35389  satffunlem2lem1  35391  fgmin  36358  nndivsub  36445  mblfinlem3  37653  rngonegrmul  37938  crngm23  37996  hlrelat2  39397  pmaple  39755  pmodlem2  39841  dalaw  39880  sn-sup2  42479  syl5imp  44502  com3rgbi  44504  ee223  44624  relpmin  44942  2tceilhalfelfzo1  47333  iccpartigtl  47424  iccelpart  47434  lighneallem3  47608  bgoldbtbndlem3  47808  uhgrimisgrgric  47931  clnbgrgrim  47934  clnbgr3stgrgrlic  48011  gpgusgralem  48047  gpgvtxedg0  48054  gpgvtxedg1  48055  ply1mulgsumlem1  48375  fllog2  48557