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  4421  fimacnvdisj  5445  fvimacnv  5680  ssct  6886  f1vrnfibi  7020  inl11  7140  ctssdc  7188  enomnilem  7213  enmkvlem  7236  djuen  7296  cauappcvgprlemlol  7733  cauappcvgprlemladdru  7742  cauappcvgprlemladdrl  7743  caucvgprlemlol  7756  caucvgprlemladdrl  7764  caucvgprprlemlol  7784  suplocsrlem  7894  recgt1i  8944  avgle2  9252  xnn0le2is012  9960  ioodisj  10087  fzneuz  10195  zsupcllemstep  10338  fihashfn  10911  shftfvalg  11002  shftfval  11005  cvg1nlemres  11169  resqrexlem1arp  11189  maxabslemval  11392  xrmaxiflemval  11434  xrmaxadd  11445  xrminmax  11449  summodclem3  11564  fsumsplit  11591  mertenslemub  11718  fprodsplit  11781  demoivreALT  11958  bitsp1  12135  gcdneg  12176  bezoutlemsup  12203  eucalginv  12251  eucalg  12254  odzdvds  12441  pclemdc  12484  fldivp1  12544  prmunb  12558  enctlem  12676  ctiunctlemfo  12683  pwssnf1o  13002  intopsn  13071  grpsubval  13250  mulgnndir  13359  gsumfzreidx  13545  gsumfzmptfidmadd  13547  znunit  14293  iscnp4  14562  cnntr  14569  tx2cn  14614  hmeontr  14657  hmeores  14659  xmetres2  14723  metres2  14725  limccnp2cntop  15021  limccoap  15022  isomninnlem  15787  iswomninnlem  15806  ismkvnnlem  15809