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  4488  fimacnvdisj  5529  fvimacnv  5771  ssct  7043  f1vrnfibi  7187  inl11  7307  ctssdc  7355  enomnilem  7380  enmkvlem  7403  djuen  7469  cauappcvgprlemlol  7910  cauappcvgprlemladdru  7919  cauappcvgprlemladdrl  7920  caucvgprlemlol  7933  caucvgprlemladdrl  7941  caucvgprprlemlol  7961  suplocsrlem  8071  recgt1i  9120  avgle2  9428  eluzmn  9806  xnn0le2is012  10145  ioodisj  10272  fzneuz  10381  zsupcllemstep  10535  fihashfn  11109  shftfvalg  11441  shftfval  11444  cvg1nlemres  11608  resqrexlem1arp  11628  maxabslemval  11831  xrmaxiflemval  11873  xrmaxadd  11884  xrminmax  11888  summodclem3  12004  fsumsplit  12031  mertenslemub  12158  fprodsplit  12221  demoivreALT  12398  bitsp1  12575  gcdneg  12616  bezoutlemsup  12643  eucalginv  12691  eucalg  12694  odzdvds  12881  pclemdc  12924  fldivp1  12984  prmunb  12998  enctlem  13116  ctiunctlemfo  13123  pwssnf1o  13444  intopsn  13513  grpsubval  13692  mulgnndir  13801  gsumfzreidx  13987  gsumfzmptfidmadd  13989  znunit  14738  iscnp4  15012  cnntr  15019  tx2cn  15064  hmeontr  15107  hmeores  15109  xmetres2  15173  metres2  15175  limccnp2cntop  15471  limccoap  15472  isomninnlem  16745  iswomninnlem  16765  ismkvnnlem  16768  gfsumval  16792