Theorem sylancom 411

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 108	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
3		sylancom.2	. 2 ⊢ ((𝜒 ∧ 𝜓) → 𝜃)
4	1, 2, 3	syl2anc 403	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 102

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

This theorem is referenced by:  ordin  4140  fimacnvdisj  5094  fvimacnv  5303  f1vrnfibi  6394  cauappcvgprlemlol  6837  cauappcvgprlemladdru  6846  cauappcvgprlemladdrl  6847  caucvgprlemlol  6860  caucvgprlemladdrl  6868  caucvgprprlemlol  6888  recgt1i  7976  avgle2  8272  ioodisj  9015  fzneuz  9118  shftfvalg  9706  shftfval  9709  cvg1nlemres  9871  resqrexlem1arp  9891  maxabslemval  10094  zsupcllemstep  10341  gcdsupex  10349  gcdsupcl  10350  gcdneg  10373  bezoutlemsup  10398  eucalginv  10438  eucialg  10441