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

Theorem syld3an3 1283
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 997 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ph )
2 simp2 998 . 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 1238 1  |-  ( (
ph  /\  ps  /\  ch )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 978
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117  df-3an 980
This theorem is referenced by:  syld3an1  1284  syld3an2  1285  brelrng  4860  moriotass  5861  nnncan1  8195  lediv1  8828  modqval  10326  modqvalr  10327  modqcl  10328  flqpmodeq  10329  modq0  10331  modqge0  10334  modqlt  10335  modqdiffl  10337  modqdifz  10338  modqvalp1  10345  exp3val  10524  bcval4  10734  dvdsmultr1  11840  dvdssub2  11844  divalglemeuneg  11930  ndvdsadd  11938  grpsubf  12954  grpinvsub  12957  grpnpcan  12967  mulginvcom  13013  mulginvinv  13014  subgsubcl  13050  dvrcl  13309  unitdvcl  13310  basgen2  13620  opnneiss  13697  cnpf2  13746  sincosq1lem  14285
  Copyright terms: Public domain W3C validator