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  4480  fimacnvdisj  5518  fvimacnv  5758  ssct  6995  f1vrnfibi  7135  inl11  7255  ctssdc  7303  enomnilem  7328  enmkvlem  7351  djuen  7416  cauappcvgprlemlol  7857  cauappcvgprlemladdru  7866  cauappcvgprlemladdrl  7867  caucvgprlemlol  7880  caucvgprlemladdrl  7888  caucvgprprlemlol  7908  suplocsrlem  8018  recgt1i  9068  avgle2  9376  eluzmn  9752  xnn0le2is012  10091  ioodisj  10218  fzneuz  10326  zsupcllemstep  10479  fihashfn  11053  shftfvalg  11369  shftfval  11372  cvg1nlemres  11536  resqrexlem1arp  11556  maxabslemval  11759  xrmaxiflemval  11801  xrmaxadd  11812  xrminmax  11816  summodclem3  11931  fsumsplit  11958  mertenslemub  12085  fprodsplit  12148  demoivreALT  12325  bitsp1  12502  gcdneg  12543  bezoutlemsup  12570  eucalginv  12618  eucalg  12621  odzdvds  12808  pclemdc  12851  fldivp1  12911  prmunb  12925  enctlem  13043  ctiunctlemfo  13050  pwssnf1o  13371  intopsn  13440  grpsubval  13619  mulgnndir  13728  gsumfzreidx  13914  gsumfzmptfidmadd  13916  znunit  14663  iscnp4  14932  cnntr  14939  tx2cn  14984  hmeontr  15027  hmeores  15029  xmetres2  15093  metres2  15095  limccnp2cntop  15391  limccoap  15392  isomninnlem  16570  iswomninnlem  16589  ismkvnnlem  16592