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  4475  fimacnvdisj  5509  fvimacnv  5749  ssct  6973  f1vrnfibi  7108  inl11  7228  ctssdc  7276  enomnilem  7301  enmkvlem  7324  djuen  7389  cauappcvgprlemlol  7830  cauappcvgprlemladdru  7839  cauappcvgprlemladdrl  7840  caucvgprlemlol  7853  caucvgprlemladdrl  7861  caucvgprprlemlol  7881  suplocsrlem  7991  recgt1i  9041  avgle2  9349  xnn0le2is012  10058  ioodisj  10185  fzneuz  10293  zsupcllemstep  10444  fihashfn  11017  shftfvalg  11324  shftfval  11327  cvg1nlemres  11491  resqrexlem1arp  11511  maxabslemval  11714  xrmaxiflemval  11756  xrmaxadd  11767  xrminmax  11771  summodclem3  11886  fsumsplit  11913  mertenslemub  12040  fprodsplit  12103  demoivreALT  12280  bitsp1  12457  gcdneg  12498  bezoutlemsup  12525  eucalginv  12573  eucalg  12576  odzdvds  12763  pclemdc  12806  fldivp1  12866  prmunb  12880  enctlem  12998  ctiunctlemfo  13005  pwssnf1o  13326  intopsn  13395  grpsubval  13574  mulgnndir  13683  gsumfzreidx  13869  gsumfzmptfidmadd  13871  znunit  14617  iscnp4  14886  cnntr  14893  tx2cn  14938  hmeontr  14981  hmeores  14983  xmetres2  15047  metres2  15049  limccnp2cntop  15345  limccoap  15346  isomninnlem  16357  iswomninnlem  16376  ismkvnnlem  16379