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

Theorem sylan2b 282
Description: A syllogism inference. (Contributed by NM, 21-Apr-1994.)
Hypotheses
Ref Expression
sylan2b.1  |-  ( ph  <->  ch )
sylan2b.2  |-  ( ( ps  /\  ch )  ->  th )
Assertion
Ref Expression
sylan2b  |-  ( ( ps  /\  ph )  ->  th )

Proof of Theorem sylan2b
StepHypRef Expression
1 sylan2b.1 . . 3  |-  ( ph  <->  ch )
21biimpi 119 . 2  |-  ( ph  ->  ch )
3 sylan2b.2 . 2  |-  ( ( ps  /\  ch )  ->  th )
42, 3sylan2 281 1  |-  ( ( ps  /\  ph )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    <-> wb 104
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  syl2anb  286  dcor  882  bm1.1  2074  eqtr3  2108  morex  2802  reuss2  3282  reupick  3286  rabsneu  3521  opabss  3910  triun  3957  poirr  4145  wepo  4197  wetrep  4198  rexxfrd  4300  reg3exmidlemwe  4409  nnsuc  4445  fnfco  5200  fun11iun  5289  fnressn  5499  fvpr1g  5519  fvtp1g  5521  fvtp3g  5523  fvtp3  5526  f1mpt  5566  caovlem2d  5853  offval  5879  dfoprab3  5977  1stconst  6002  2ndconst  6003  poxp  6013  tfrlemisucaccv  6106  tfr1onlemsucaccv  6122  tfrcllemsucaccv  6135  fiintim  6695  addclpi  6949  addnidpig  6958  reapmul1  8135  nnnn0addcl  8766  un0addcl  8769  un0mulcl  8770  zltnle  8859  nn0ge0div  8896  uzind3  8922  uzind4  9139  ltsubrp  9231  ltaddrp  9232  xrlttr  9328  xrltso  9329  xltnegi  9360  fzind2  9713  qltnle  9720  qbtwnxr  9732  exp3vallem  10019  expp1  10025  expnegap0  10026  expcllem  10029  mulexpzap  10058  expaddzap  10062  expmulzap  10064  hashunlem  10275  shftf  10327  sqrtdiv  10538  mulcn2  10764  isummolem2  10835  cvgratz  10989  dvdsflip  11193  dvdsfac  11202  lcmgcdlem  11400  rpexp1i  11474  hashdvds  11538  hashgcdlem  11544  bj-bdfindes  12148  bj-findes  12180
  Copyright terms: Public domain W3C validator