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  4506  fimacnvdisj  5551  fvimacnv  5793  ssct  7067  f1vrnfibi  7212  inl11  7356  ctssdc  7404  enomnilem  7429  enmkvlem  7452  djuen  7518  cauappcvgprlemlol  7962  cauappcvgprlemladdru  7971  cauappcvgprlemladdrl  7972  caucvgprlemlol  7985  caucvgprlemladdrl  7993  caucvgprprlemlol  8013  suplocsrlem  8123  recgt1i  9172  avgle2  9480  eluzmn  9860  xnn0le2is012  10199  ioodisj  10326  fzneuz  10435  zsupcllemstep  10589  fihashfn  11164  sseqn  11203  shftfvalg  11503  shftfval  11506  cvg1nlemres  11670  resqrexlem1arp  11690  maxabslemval  11893  xrmaxiflemval  11935  xrmaxadd  11946  xrminmax  11950  summodclem3  12066  fsumsplit  12093  mertenslemub  12220  fprodsplit  12283  demoivreALT  12460  bitsp1  12637  gcdneg  12678  bezoutlemsup  12705  eucalginv  12753  eucalg  12756  odzdvds  12943  pclemdc  12986  fldivp1  13046  prmunb  13060  enctlem  13183  ctiunctlemfo  13190  pwssnf1o  13511  intopsn  13580  grpsubval  13759  mulgnndir  13868  gsumfzreidx  14054  gsumfzmptfidmadd  14056  znunit  14807  iscnp4  15083  cnntr  15090  tx2cn  15135  hmeontr  15178  hmeores  15180  xmetres2  15244  metres2  15246  limccnp2cntop  15542  limccoap  15543  isomninnlem  16814  iswomninnlem  16834  ismkvnnlem  16837  gfsumval  16862