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  4482  fimacnvdisj  5521  fvimacnv  5762  ssct  6999  f1vrnfibi  7143  inl11  7263  ctssdc  7311  enomnilem  7336  enmkvlem  7359  djuen  7425  cauappcvgprlemlol  7866  cauappcvgprlemladdru  7875  cauappcvgprlemladdrl  7876  caucvgprlemlol  7889  caucvgprlemladdrl  7897  caucvgprprlemlol  7917  suplocsrlem  8027  recgt1i  9077  avgle2  9385  eluzmn  9761  xnn0le2is012  10100  ioodisj  10227  fzneuz  10335  zsupcllemstep  10488  fihashfn  11062  shftfvalg  11378  shftfval  11381  cvg1nlemres  11545  resqrexlem1arp  11565  maxabslemval  11768  xrmaxiflemval  11810  xrmaxadd  11821  xrminmax  11825  summodclem3  11940  fsumsplit  11967  mertenslemub  12094  fprodsplit  12157  demoivreALT  12334  bitsp1  12511  gcdneg  12552  bezoutlemsup  12579  eucalginv  12627  eucalg  12630  odzdvds  12817  pclemdc  12860  fldivp1  12920  prmunb  12934  enctlem  13052  ctiunctlemfo  13059  pwssnf1o  13380  intopsn  13449  grpsubval  13628  mulgnndir  13737  gsumfzreidx  13923  gsumfzmptfidmadd  13925  znunit  14672  iscnp4  14941  cnntr  14948  tx2cn  14993  hmeontr  15036  hmeores  15038  xmetres2  15102  metres2  15104  limccnp2cntop  15400  limccoap  15401  isomninnlem  16634  iswomninnlem  16653  ismkvnnlem  16656  gfsumval  16680