Theorem sylancom 416

Description: Syllogism inference with commutation of antecents. (Contributed by NM, 2-Jul-2008.)

Hypotheses

Ref	Expression
sylancom.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)
sylancom.2	⊢ ((𝜒 ∧ 𝜓) → 𝜃)

Assertion

Ref	Expression
sylancom	⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Proof of Theorem sylancom

Step	Hyp	Ref	Expression
1		sylancom.1	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2		simpr 109	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
3		sylancom.2	. 2 ⊢ ((𝜒 ∧ 𝜓) → 𝜃)
4	1, 2, 3	syl2anc 408	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  ordin  4307  fimacnvdisj  5307  fvimacnv  5535  ssct  6712  f1vrnfibi  6833  inl11  6950  ctssdc  6998  enomnilem  7010  djuen  7067  cauappcvgprlemlol  7455  cauappcvgprlemladdru  7464  cauappcvgprlemladdrl  7465  caucvgprlemlol  7478  caucvgprlemladdrl  7486  caucvgprprlemlol  7506  suplocsrlem  7616  recgt1i  8656  avgle2  8961  xnn0le2is012  9649  ioodisj  9776  fzneuz  9881  fihashfn  10546  shftfvalg  10590  shftfval  10593  cvg1nlemres  10757  resqrexlem1arp  10777  maxabslemval  10980  xrmaxiflemval  11019  xrmaxadd  11030  xrminmax  11034  summodclem3  11149  fsumsplit  11176  mertenslemub  11303  demoivreALT  11480  zsupcllemstep  11638  gcdsupex  11646  gcdsupcl  11647  gcdneg  11670  bezoutlemsup  11697  eucalginv  11737  eucalg  11740  enctlem  11945  ctiunctlemfo  11952  iscnp4  12387  cnntr  12394  tx2cn  12439  hmeontr  12482  hmeores  12484  xmetres2  12548  metres2  12550  limccnp2cntop  12815  limccoap  12816  isomninnlem  13225