Theorem sylancom 414

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 406	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  ordin  4265  fimacnvdisj  5263  fvimacnv  5487  ssct  6663  f1vrnfibi  6783  inl11  6900  ctssdc  6948  enomnilem  6958  djuen  7012  cauappcvgprlemlol  7397  cauappcvgprlemladdru  7406  cauappcvgprlemladdrl  7407  caucvgprlemlol  7420  caucvgprlemladdrl  7428  caucvgprprlemlol  7448  recgt1i  8560  avgle2  8859  xnn0le2is012  9536  ioodisj  9663  fzneuz  9768  fihashfn  10433  shftfvalg  10477  shftfval  10480  cvg1nlemres  10643  resqrexlem1arp  10663  maxabslemval  10866  xrmaxiflemval  10905  xrmaxadd  10916  xrminmax  10920  summodclem3  11035  fsumsplit  11062  mertenslemub  11189  demoivreALT  11324  zsupcllemstep  11480  gcdsupex  11488  gcdsupcl  11489  gcdneg  11512  bezoutlemsup  11537  eucalginv  11577  eucalg  11580  ctiunctlemfo  11789  iscnp4  12223  cnntr  12230  tx2cn  12275  xmetres2  12362  metres2  12364  limccnp2cntop  12596  isomninnlem  12906