Theorem sylancom 420

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

Syntax hints:   → wi 4   ∧ wa 104

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

This theorem is referenced by:  ordin  4482  fimacnvdisj  5521  fvimacnv  5762  ssct  7000  f1vrnfibi  7144  inl11  7264  ctssdc  7312  enomnilem  7337  enmkvlem  7360  djuen  7426  cauappcvgprlemlol  7867  cauappcvgprlemladdru  7876  cauappcvgprlemladdrl  7877  caucvgprlemlol  7890  caucvgprlemladdrl  7898  caucvgprprlemlol  7918  suplocsrlem  8028  recgt1i  9078  avgle2  9386  eluzmn  9762  xnn0le2is012  10101  ioodisj  10228  fzneuz  10336  zsupcllemstep  10490  fihashfn  11064  shftfvalg  11383  shftfval  11386  cvg1nlemres  11550  resqrexlem1arp  11570  maxabslemval  11773  xrmaxiflemval  11815  xrmaxadd  11826  xrminmax  11830  summodclem3  11946  fsumsplit  11973  mertenslemub  12100  fprodsplit  12163  demoivreALT  12340  bitsp1  12517  gcdneg  12558  bezoutlemsup  12585  eucalginv  12633  eucalg  12636  odzdvds  12823  pclemdc  12866  fldivp1  12926  prmunb  12940  enctlem  13058  ctiunctlemfo  13065  pwssnf1o  13386  intopsn  13455  grpsubval  13634  mulgnndir  13743  gsumfzreidx  13929  gsumfzmptfidmadd  13931  znunit  14679  iscnp4  14948  cnntr  14955  tx2cn  15000  hmeontr  15043  hmeores  15045  xmetres2  15109  metres2  15111  limccnp2cntop  15407  limccoap  15408  isomninnlem  16660  iswomninnlem  16680  ismkvnnlem  16683  gfsumval  16707