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

Theorem syld3an3 1244
Description: A syllogism inference. (Contributed by NM, 20-May-2007.)
Hypotheses
Ref Expression
syld3an3.1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
syld3an3.2  |-  ( (
ph  /\  ps  /\  th )  ->  ta )
Assertion
Ref Expression
syld3an3  |-  ( (
ph  /\  ps  /\  ch )  ->  ta )

Proof of Theorem syld3an3
StepHypRef Expression
1 simp1 964 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ph )
2 simp2 965 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ps )
3 syld3an3.1 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
4 syld3an3.2 . 2  |-  ( (
ph  /\  ps  /\  th )  ->  ta )
51, 2, 3, 4syl3anc 1199 1  |-  ( (
ph  /\  ps  /\  ch )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 945
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 947
This theorem is referenced by:  syld3an1  1245  syld3an2  1246  brelrng  4738  moriotass  5724  nnncan1  7962  lediv1  8584  modqval  10037  modqvalr  10038  modqcl  10039  flqpmodeq  10040  modq0  10042  modqge0  10045  modqlt  10046  modqdiffl  10048  modqdifz  10049  modqvalp1  10056  exp3val  10235  bcval4  10438  dvdsmultr1  11427  dvdssub2  11431  divalglemeuneg  11516  ndvdsadd  11524  basgen2  12145  opnneiss  12222  cnpf2  12271
  Copyright terms: Public domain W3C validator