Theorem sylancom 424

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 415	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107  ax-ia3 108

This theorem is used by:  ordin  4532  fimacnvdisj  5579  fvimacnv  5827  ssct  7118  f1vrnfibi  7263  inl11  7411  ctssdc  7459  enomnilem  7484  enmkvlem  7507  djuen  7573  cauappcvgprlemlol  8020  cauappcvgprlemladdru  8029  cauappcvgprlemladdrl  8030  caucvgprlemlol  8043  caucvgprlemladdrl  8051  caucvgprprlemlol  8071  suplocsrlem  8181  recgt1i  9236  avgle2  9558  eluzmn  9944  xnn0le2is012  10285  ioodisj  10412  fzneuz  10525  zsupcllemstep  10679  fihashfn  11262  sseqn  11301  shftfvalg  11605  shftfval  11608  cvg1nlemres  11773  resqrexlem1arp  11793  maxabslemval  11997  xrmaxiflemval  12041  xrmaxadd  12052  xrminmax  12056  summodclem3  12172  fsumsplit  12199  mertenslemub  12326  fprodsplit  12389  demoivreALT  12566  bitsp1  12743  gcdneg  12784  bezoutlemsup  12811  eucalginv  12859  eucalg  12862  odzdvds  13053  pclemdc  13096  fldivp1  13156  prmunb  13170  ballotfilemirc  13333  enctlem  13381  ctiunctlemfo  13388  intopsn  13746  grpsubval  13910  mulgnndir  14013  cntzidss  14172  gzsumreidx  14231  gsumvalfi  14242  gsumf1ofi  14250  pwssnf1o  14318  znunit  15103  iscnp4  15444  cnntr  15451  tx2cn  15496  hmeontr  15539  hmeores  15541  xmetres2  15605  metres2  15607  limccnp2cntop  15903  limccoap  15904  birthdaylem3  16227  isomninnlem  17285  iswomninnlem  17306  ismkvnnlem  17309