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

Theorem syl12anc 1144
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 )
syl12anc.4  |-  ( ( ps  /\  ( ch 
/\  th ) )  ->  ta )
Assertion
Ref Expression
syl12anc  |-  ( ph  ->  ta )

Proof of Theorem syl12anc
StepHypRef Expression
1 sylXanc.1 . . 3  |-  ( ph  ->  ps )
2 sylXanc.2 . . 3  |-  ( ph  ->  ch )
3 sylXanc.3 . . 3  |-  ( ph  ->  th )
41, 2, 3jca32 297 . 2  |-  ( ph  ->  ( ps  /\  ( ch  /\  th ) ) )
5 syl12anc.4 . 2  |-  ( ( ps  /\  ( ch 
/\  th ) )  ->  ta )
64, 5syl 14 1  |-  ( ph  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 105
This theorem is referenced by:  syl22anc  1147  cocan1  5455  fliftfun  5464  isopolem  5489  f1oiso2  5494  caovcld  5682  caovcomd  5685  tfrlemisucaccv  5970  fidceq  6361  findcard2d  6379  diffifi  6382  supisolem  6412  ordiso2  6415  prarloclemup  6651  prarloc  6659  nqprl  6707  nqpru  6708  ltaddpr  6753  aptiprlemu  6796  archpr  6799  cauappcvgprlem2  6816  caucvgprlem2  6836  caucvgprprlem2  6866  recexgt0sr  6916  archsr  6924  conjmulap  7780  lerec2  7930  ledivp1  7944  cju  7989  nn2ge  8022  gtndiv  8393  z2ge  8840  iccssioo2  8916  fzrev3  9051  elfz1b  9054  qbtwnzlemstep  9205  qbtwnzlemex  9207  rebtwn2zlemstep  9209  rebtwn2z  9211  qbtwnre  9213  flqdiv  9271  iseqcaopr  9406  expnegzap  9454  caucvgrelemrec  9806  resqrexlemex  9852
  Copyright terms: Public domain W3C validator