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  4417  fimacnvdisj  5439  fvimacnv  5674  ssct  6874  f1vrnfibi  7006  inl11  7126  ctssdc  7174  enomnilem  7199  enmkvlem  7222  djuen  7273  cauappcvgprlemlol  7709  cauappcvgprlemladdru  7718  cauappcvgprlemladdrl  7719  caucvgprlemlol  7732  caucvgprlemladdrl  7740  caucvgprprlemlol  7760  suplocsrlem  7870  recgt1i  8919  avgle2  9227  xnn0le2is012  9935  ioodisj  10062  fzneuz  10170  fihashfn  10874  shftfvalg  10965  shftfval  10968  cvg1nlemres  11132  resqrexlem1arp  11152  maxabslemval  11355  xrmaxiflemval  11396  xrmaxadd  11407  xrminmax  11411  summodclem3  11526  fsumsplit  11553  mertenslemub  11680  fprodsplit  11743  demoivreALT  11920  zsupcllemstep  12085  gcdneg  12122  bezoutlemsup  12149  eucalginv  12197  eucalg  12200  odzdvds  12386  pclemdc  12429  fldivp1  12489  prmunb  12503  enctlem  12592  ctiunctlemfo  12599  intopsn  12953  grpsubval  13121  mulgnndir  13224  gsumfzreidx  13410  gsumfzmptfidmadd  13412  znunit  14158  iscnp4  14397  cnntr  14404  tx2cn  14449  hmeontr  14492  hmeores  14494  xmetres2  14558  metres2  14560  limccnp2cntop  14856  limccoap  14857  isomninnlem  15590  iswomninnlem  15609  ismkvnnlem  15612