Theorem sylancom 424

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107  ax-ia3 108

This theorem is used by:  ordin  4530  fimacnvdisj  5576  fvimacnv  5824  ssct  7114  f1vrnfibi  7259  inl11  7405  ctssdc  7453  enomnilem  7478  enmkvlem  7501  djuen  7567  cauappcvgprlemlol  8014  cauappcvgprlemladdru  8023  cauappcvgprlemladdrl  8024  caucvgprlemlol  8037  caucvgprlemladdrl  8045  caucvgprprlemlol  8065  suplocsrlem  8175  recgt1i  9228  avgle2  9547  eluzmn  9928  xnn0le2is012  10268  ioodisj  10395  fzneuz  10508  zsupcllemstep  10662  fihashfn  11240  sseqn  11279  shftfvalg  11583  shftfval  11586  cvg1nlemres  11751  resqrexlem1arp  11771  maxabslemval  11974  xrmaxiflemval  12016  xrmaxadd  12027  xrminmax  12031  summodclem3  12147  fsumsplit  12174  mertenslemub  12301  fprodsplit  12364  demoivreALT  12541  bitsp1  12718  gcdneg  12759  bezoutlemsup  12786  eucalginv  12834  eucalg  12837  odzdvds  13024  pclemdc  13067  fldivp1  13127  prmunb  13141  ballotfilemirc  13275  enctlem  13323  ctiunctlemfo  13330  intopsn  13687  grpsubval  13851  mulgnndir  13954  gzsumreidx  14141  gsumvalfi  14152  gsumf1ofi  14160  pwssnf1o  14211  znunit  14994  iscnp4  15319  cnntr  15326  tx2cn  15371  hmeontr  15414  hmeores  15416  xmetres2  15480  metres2  15482  limccnp2cntop  15778  limccoap  15779  birthdaylem3  16089  isomninnlem  17079  iswomninnlem  17099  ismkvnnlem  17102