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  4403  fimacnvdisj  5419  fvimacnv  5651  ssct  6843  f1vrnfibi  6973  inl11  7093  ctssdc  7141  enomnilem  7165  enmkvlem  7188  djuen  7239  cauappcvgprlemlol  7675  cauappcvgprlemladdru  7684  cauappcvgprlemladdrl  7685  caucvgprlemlol  7698  caucvgprlemladdrl  7706  caucvgprprlemlol  7726  suplocsrlem  7836  recgt1i  8884  avgle2  9189  xnn0le2is012  9895  ioodisj  10022  fzneuz  10130  fihashfn  10811  shftfvalg  10858  shftfval  10861  cvg1nlemres  11025  resqrexlem1arp  11045  maxabslemval  11248  xrmaxiflemval  11289  xrmaxadd  11300  xrminmax  11304  summodclem3  11419  fsumsplit  11446  mertenslemub  11573  fprodsplit  11636  demoivreALT  11812  zsupcllemstep  11977  gcdneg  12014  bezoutlemsup  12041  eucalginv  12087  eucalg  12090  odzdvds  12276  pclemdc  12319  fldivp1  12379  prmunb  12393  enctlem  12482  ctiunctlemfo  12489  intopsn  12840  grpsubval  12987  mulgnndir  13088  iscnp4  14170  cnntr  14177  tx2cn  14222  hmeontr  14265  hmeores  14267  xmetres2  14331  metres2  14333  limccnp2cntop  14598  limccoap  14599  isomninnlem  15232  iswomninnlem  15251  ismkvnnlem  15254