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

Theorem syl21anc 1169
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  4082  brcogw  4532  funprg  4980  funtpg  4981  fnunsn  5037  ftpg  5379  fsnunf  5394  isotr  5487  off  5755  caofrss  5766  tfr1onlembxssdm  5992  tfrcllembxssdm  6005  ac6sfi  6431  mulclpi  6580  archnqq  6669  addlocprlemlt  6783  addlocprlemeq  6785  addlocprlemgt  6786  mullocprlem  6822  apreim  7770  ltrec1  8033  divge0d  8895  fseq1p1m1  9187  q2submod  9467  iseqoveq  9540  iseqcaopr2  9557  iseqdistr  9567  facavg  9770  shftfibg  9846  sqrtdiv  10066  sqrtdivd  10192  mulcn2  10289  dvdslegcd  10500  gcdnncl  10503  qredeu  10623  rpdvds  10625  rpexp  10676  oddpwdclemodd  10694
  Copyright terms: Public domain W3C validator