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  3559  po2nr  5543  wefrc  5615  tz7.7  6339  funssres  6532  isomin  7279  f1ocnv2d  7607  onint  7731  f1oweALT  7912  bropfvvvv  8030  tfrlem9  8312  tz7.49  8372  oelim  8457  oaordex  8481  omordi  8489  omass  8503  oen0  8509  nnmass  8547  nnmordi  8554  inf3lem2  9528  epfrs  9630  indcardi  9941  ackbij1lem16  10134  cfcoflem  10172  axcc3  10338  zorn2lem7  10402  grur1a  10719  genpcd  10906  genpnmax  10907  mulclprlem  10919  distrlem1pr  10925  ltaddpr  10934  ltexprlem6  10941  ltexprlem7  10942  mulgt0sr  11005  divgt0  11999  divge0  12000  sup2  12087  uzind2  12574  uzwo  12813  supxrun  13219  expnbnd  14143  facdiv  14198  hashimarni  14352  swrdswrdlem  14615  wrd2ind  14634  s3iunsndisj  14879  caubnd  15270  dvdsabseq  16228  lcmfunsnlem2lem1  16553  divgcdcoprm0  16580  ncoprmlnprm  16643  cshwshashlem1  17011  psgnunilem4  19413  lmodvsdi  20822  xrsdsreclblem  21353  nzerooringczr  21421  cpmatacl  22634  riinopn  22826  0ntr  22989  elcls  22991  hausnei2  23271  fgfil  23793  alexsubALTlem2  23966  alexsubALT  23969  aalioulem3  26272  aalioulem4  26273  wilthlem3  27010  2sqreultlem  27388  2sqreunnltlem  27391  finsumvtxdg2size  29533  upgrewlkle2  29589  upgrwlkdvdelem  29718  uhgrwkspthlem2  29736  clwwlkinwwlk  30024  wwlksext2clwwlk  30041  1pthon2v  30137  n4cyclfrgr  30275  frgrnbnb  30277  frgrwopreglem4a  30294  frgrreg  30378  frgrregord013  30379  grpoidinvlem3  30490  elspansn5  31558  atcv1  32364  atcvatlem  32369  chirredlem3  32376  mdsymlem3  32389  mdsymlem5  32391  mdsymlem6  32392  sumdmdlem2  32403  f1o3d  32612  slmdvsdi  33193  satfv0fun  35438  satffunlem1lem1  35469  satffunlem2lem1  35471  fgmin  36437  nndivsub  36524  mblfinlem3  37722  rngonegrmul  38007  crngm23  38065  hlrelat2  39525  pmaple  39883  pmodlem2  39969  dalaw  40008  sn-sup2  42612  syl5imp  44632  com3rgbi  44634  ee223  44754  relpmin  45072  2tceilhalfelfzo1  47459  iccpartigtl  47550  iccelpart  47560  lighneallem3  47734  bgoldbtbndlem3  47934  uhgrimisgrgric  48058  clnbgrgrim  48061  clnbgr3stgrgrlic  48147  gpgusgralem  48183  gpgvtxedg0  48190  gpgvtxedg1  48191  ply1mulgsumlem1  48514  fllog2  48696