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  4858  moriotass  5858  nnncan1  8192  lediv1  8825  modqval  10323  modqvalr  10324  modqcl  10325  flqpmodeq  10326  modq0  10328  modqge0  10331  modqlt  10332  modqdiffl  10334  modqdifz  10335  modqvalp1  10342  exp3val  10521  bcval4  10731  dvdsmultr1  11837  dvdssub2  11841  divalglemeuneg  11927  ndvdsadd  11935  grpsubf  12948  grpinvsub  12951  grpnpcan  12961  mulginvcom  13006  mulginvinv  13007  subgsubcl  13043  dvrcl  13302  unitdvcl  13303  basgen2  13517  opnneiss  13594  cnpf2  13643  sincosq1lem  14182
  Copyright terms: Public domain W3C validator