ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  syl21anc Unicode version

Theorem syl21anc 1173
Description: Syllogism combined with contraction. (Contributed by Jeff Hankins, 1-Aug-2009.)
Hypotheses
Ref Expression
sylXanc.1  |-  ( ph  ->  ps )
sylXanc.2  |-  ( ph  ->  ch )
sylXanc.3  |-  ( ph  ->  th )
syl21anc.4  |-  ( ( ( ps  /\  ch )  /\  th )  ->  ta )
Assertion
Ref Expression
syl21anc  |-  ( ph  ->  ta )

Proof of Theorem syl21anc
StepHypRef Expression
1 sylXanc.1 . . 3  |-  ( ph  ->  ps )
2 sylXanc.2 . . 3  |-  ( ph  ->  ch )
3 sylXanc.3 . . 3  |-  ( ph  ->  th )
41, 2, 3jca31 302 . 2  |-  ( ph  ->  ( ( ps  /\  ch )  /\  th )
)
5 syl21anc.4 . 2  |-  ( ( ( ps  /\  ch )  /\  th )  ->  ta )
64, 5syl 14 1  |-  ( ph  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 106
This theorem is referenced by:  issod  4137  brcogw  4593  funprg  5050  funtpg  5051  fnunsn  5107  ftpg  5465  fsnunf  5480  isotr  5577  off  5850  caofrss  5861  tfr1onlembxssdm  6090  tfrcllembxssdm  6103  pmresg  6413  ac6sfi  6594  tridc  6595  fidcenumlemrks  6641  sbthlemi8  6652  casefun  6755  caseinj  6759  djufun  6763  djuinj  6765  mulclpi  6866  archnqq  6955  addlocprlemlt  7069  addlocprlemeq  7071  addlocprlemgt  7072  mullocprlem  7108  apreim  8056  ltrec1  8321  divge0d  9183  fseq1p1m1  9475  q2submod  9757  iseqoveq  9850  iseqcaopr2  9876  iseqdistr  9910  seq3distr  9911  facavg  10119  shftfibg  10219  sqrtdiv  10440  sqrtdivd  10566  mulcn2  10665  dvdslegcd  11038  gcdnncl  11041  qredeu  11161  rpdvds  11163  rpexp  11214  oddpwdclemodd  11232  divnumden  11256  divdenle  11257  phimullem  11283
  Copyright terms: Public domain W3C validator