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

Theorem syl21anc 1198
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 305 . 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 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107
This theorem is referenced by:  issod  4209  brcogw  4676  funprg  5141  funtpg  5142  fnunsn  5198  ftpg  5570  fsnunf  5586  isotr  5683  off  5960  caofrss  5972  tfr1onlembxssdm  6206  tfrcllembxssdm  6219  pmresg  6536  ac6sfi  6758  tridc  6759  fidcenumlemrks  6807  sbthlemi8  6818  casefun  6936  caseinj  6940  djufun  6955  djuinj  6957  mulclpi  7100  archnqq  7189  addlocprlemlt  7303  addlocprlemeq  7305  addlocprlemgt  7306  mullocprlem  7342  apreim  8328  ltrec1  8603  divge0d  9470  fseq1p1m1  9814  q2submod  10098  seq3caopr2  10195  seq3distr  10226  facavg  10432  shftfibg  10532  sqrtdiv  10754  sqrtdivd  10880  mulcn2  11021  demoivreALT  11378  dvdslegcd  11549  gcdnncl  11552  qredeu  11674  rpdvds  11676  rpexp  11727  oddpwdclemodd  11745  divnumden  11769  divdenle  11770  phimullem  11796  setsfun  11889  setsfun0  11890  strleund  11942  comet  12563  fsumcncntop  12620  mulcncf  12655  trilpo  13038
  Copyright terms: Public domain W3C validator