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 ⊢ (𝜑 → (𝜓 → (𝜃 → (𝜒 → 𝜏))))

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  93  com35  99  3an1rs  1376  rspct  3570  po2nr  5573  wefrc  5645  tz7.7  6375  funssres  6569  isomin  7325  f1ocnv2d  7653  onint  7777  f1oweALT  7957  bropfvvvv  8075  tfrlem9  8360  tz7.49  8420  oelim  8507  oaordex  8531  omordi  8539  omass  8553  oen0  8560  nnmass  8598  nnmordi  8605  inf3lem2  9586  epfrs  9688  indcardi  10013  ackbij1lem16  10205  cfcoflem  10244  axcc3  10410  zorn2lem7  10474  grur1a  10792  genpcd  10979  genpnmax  10980  mulclprlem  10992  distrlem1pr  10998  ltaddpr  11007  ltexprlem6  11014  ltexprlem7  11015  mulgt0sr  11078  divgt0  12071  divge0  12072  sup2  12159  uzind2  12677  uzwo  12923  supxrun  13330  expnbnd  14256  facdiv  14311  hashimarni  14466  swrdswrdlem  14729  wrd2ind  14748  s3iunsndisj  14993  caubnd  15398  dvdsabseq  16359  lcmfunsnlem2lem1  16684  divgcdcoprm0  16711  ncoprmlnprm  16775  cshwshashlem1  17143  psgnunilem4  19555  lmodvsdi  20972  xrsdsreclblem  21520  nzerooringczr  21587  cpmatacl  22830  riinopn  23022  0ntr  23185  elcls  23187  hausnei2  23467  fgfil  23989  alexsubALTlem2  24162  alexsubALT  24165  aalioulem3  26452  aalioulem4  26453  wilthlem3  27188  2sqreultlem  27565  2sqreunnltlem  27568  bdayfinbndlem1  28614  finsumvtxdg2size  29805  upgrewlkle2  29861  upgrwlkdvdelem  29990  uhgrwkspthlem2  30008  clwwlkinwwlk  30296  wwlksext2clwwlk  30313  1pthon2v  30409  n4cyclfrgr  30547  frgrnbnb  30549  frgrwopreglem4a  30566  frgrreg  30650  frgrregord013  30651  grpoidinvlem3  30763  elspansn5  31831  atcv1  32637  atcvatlem  32642  chirredlem3  32649  mdsymlem3  32662  mdsymlem5  32664  mdsymlem6  32665  sumdmdlem2  32676  f1o3d  32879  slmdvsdi  33443  satfv0fun  35729  satffunlem1lem1  35760  satffunlem2lem1  35762  fgmin  36738  nndivsub  36825  mblfinlem3  38165  rngonegrmul  38450  crngm23  38508  hlrelat2  40034  pmaple  40392  pmodlem2  40478  dalaw  40517  sn-sup2  43120  syl5imp  45080  com3rgbi  45082  ee223  45202  relpmin  45520  2tceilhalfelfzo1  47929  iccpartigtl  48028  iccelpart  48038  lighneallem3  48215  bgoldbtbndlem3  48428  uhgrimisgrgric  48552  clnbgrgrim  48555  clnbgr3stgrgrlic  48641  gpgusgralem  48677  gpgvtxedg0  48684  gpgvtxedg1  48685  ply1mulgsumlem1  49018  fllog2  49200