Theorem com34 92

Description: Commutation of antecedents. Swap 3rd and 4th. Deduction associated with com23 87. Double deduction associated with com12 33. (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 91	. 2 ⊢ ((𝜒 → (𝜃 → 𝜏)) → (𝜃 → (𝜒 → 𝜏)))
3	1, 2	syl6 36	1 ⊢ (𝜑 → (𝜓 → (𝜃 → (𝜒 → 𝜏))))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  com4l  93  com35  99  3an1rs  1378  rspct  3562  po2nr  5577  wefrc  5649  tz7.7  6383  funssres  6578  isomin  7339  f1ocnv2d  7668  onint  7790  f1oweALT  7970  bropfvvvv  8090  tfrlem9  8375  tz7.49  8437  oelim  8524  oaordex  8548  omordi  8556  omass  8570  oen0  8577  nnmass  8615  nnmordi  8622  inf3lem2  9611  epfrs  9713  indcardi  10047  ackbij1lem16  10239  cfcoflem  10277  axcc3  10443  zorn2lem7  10507  grur1a  10831  genpcd  11018  genpnmax  11019  mulclprlem  11031  distrlem1pr  11037  ltaddpr  11046  ltexprlem6  11053  ltexprlem7  11054  mulgt0sr  11117  divgt0  12110  divge0  12111  sup2  12198  uzind2  12717  uzwo  12963  supxrun  13371  expnbnd  14299  facdiv  14354  hashimarni  14509  swrdswrdlem  14776  wrd2ind  14795  s3iunsndisj  15044  caubnd  15449  dvdsabseq  16406  lcmfunsnlem2lem1  16731  divgcdcoprm0  16758  ncoprmlnprm  16822  cshwshashlem1  17190  psgnunilem4  19627  lmodvsdi  21072  xrsdsreclblem  21629  nzerooringczr  21696  cpmatacl  22944  riinopn  23136  0ntr  23299  elcls  23301  hausnei2  23581  fgfil  24104  alexsubALTlem2  24277  alexsubALT  24280  aalioulem3  26573  aalioulem4  26574  wilthlem3  27309  2sqreultlem  27686  2sqreunnltlem  27689  bdayfinbndlem1  28735  finsumvtxdg2size  30013  upgrewlkle2  30069  upgrwlkdvdelem  30204  uhgrwkspthlem2  30222  clwwlkinwwlk  30513  wwlksext2clwwlk  30530  1pthon2v  30636  n4cyclfrgr  30774  frgrnbnb  30776  frgrwopreglem4a  30793  frgrreg  30877  frgrregord013  30878  grpoidinvlem3  30990  elspansn5  32058  atcv1  32864  atcvatlem  32869  chirredlem3  32876  mdsymlem3  32889  mdsymlem5  32891  mdsymlem6  32892  sumdmdlem2  32903  f1o3d  33102  slmdvsdi  33658  satfv0fun  35953  satffunlem1lem1  35984  satffunlem2lem1  35986  fgmin  36992  nndivsub  37079  mblfinlem3  38411  rngonegrmul  38697  crngm23  38755  hlrelat2  40279  pmaple  40637  pmodlem2  40723  dalaw  40762  sn-sup2  43382  syl5imp  45338  com3rgbi  45340  ee223  45460  relpmin  45778  2tceilhalfelfzo1  48227  iccpartigtl  48326  iccelpart  48336  lighneallem3  48513  bgoldbtbndlem3  48726  uhgrimisgrgric  48850  clnbgrgrim  48853  clnbgr3stgrgrlic  48939  gpgusgralem  48975  gpgvtxedg0  48982  gpgvtxedg1  48983  ply1mulgsumlem1  49319  fllog2  49501