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  4430  fimacnvdisj  5454  fvimacnv  5689  ssct  6895  f1vrnfibi  7029  inl11  7149  ctssdc  7197  enomnilem  7222  enmkvlem  7245  djuen  7305  cauappcvgprlemlol  7742  cauappcvgprlemladdru  7751  cauappcvgprlemladdrl  7752  caucvgprlemlol  7765  caucvgprlemladdrl  7773  caucvgprprlemlol  7793  suplocsrlem  7903  recgt1i  8953  avgle2  9261  xnn0le2is012  9970  ioodisj  10097  fzneuz  10205  zsupcllemstep  10353  fihashfn  10926  shftfvalg  11048  shftfval  11051  cvg1nlemres  11215  resqrexlem1arp  11235  maxabslemval  11438  xrmaxiflemval  11480  xrmaxadd  11491  xrminmax  11495  summodclem3  11610  fsumsplit  11637  mertenslemub  11764  fprodsplit  11827  demoivreALT  12004  bitsp1  12181  gcdneg  12222  bezoutlemsup  12249  eucalginv  12297  eucalg  12300  odzdvds  12487  pclemdc  12530  fldivp1  12590  prmunb  12604  enctlem  12722  ctiunctlemfo  12729  pwssnf1o  13048  intopsn  13117  grpsubval  13296  mulgnndir  13405  gsumfzreidx  13591  gsumfzmptfidmadd  13593  znunit  14339  iscnp4  14608  cnntr  14615  tx2cn  14660  hmeontr  14703  hmeores  14705  xmetres2  14769  metres2  14771  limccnp2cntop  15067  limccoap  15068  isomninnlem  15833  iswomninnlem  15852  ismkvnnlem  15855