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

Theorem syld3an3 1217
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 941 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ph )
2 simp2 942 . 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 1172 1  |-  ( (
ph  /\  ps  /\  ch )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 922
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115  df-3an 924
This theorem is referenced by:  syld3an1  1218  syld3an2  1219  brelrng  4636  moriotass  5599  nnncan1  7665  lediv1  8268  modqval  9662  modqvalr  9663  modqcl  9664  flqpmodeq  9665  modq0  9667  modqge0  9670  modqlt  9671  modqdiffl  9673  modqdifz  9674  modqvalp1  9681  expival  9859  bcval4  10060  dvdsmultr1  10740  dvdssub2  10744  divalglemeuneg  10829  ndvdsadd  10837
  Copyright terms: Public domain W3C validator