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

Theorem sylan2b 271
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 113 . 2  |-  ( ph  ->  ch )
3 sylan2b.2 . 2  |-  ( ( ps  /\  ch )  ->  th )
42, 3sylan2 270 1  |-  ( ( ps  /\  ph )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 97    <-> wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  syl2anb  275  dcor  843  bm1.1  2025  eqtr3  2059  morex  2722  reuss2  3214  reupick  3218  rabsneu  3440  opabss  3818  triun  3864  poirr  4041  rexxfrd  4182  nnsuc  4316  fnfco  5043  fun11iun  5125  fnressn  5327  fvpr1g  5345  fvtp1g  5347  fvtp3g  5349  fvtp3  5352  f1mpt  5388  caovlem2d  5671  offval  5697  dfoprab3  5795  1stconst  5820  2ndconst  5821  poxp  5831  tfrlemisucaccv  5917  addclpi  6397  addnidpig  6406  reapmul1  7553  nnnn0addcl  8175  un0addcl  8178  un0mulcl  8179  zltnle  8254  nn0ge0div  8290  uzind3  8314  uzind4  8494  ltsubrp  8579  ltaddrp  8580  xrlttr  8674  xrltso  8675  xltnegi  8706  fzind2  9053  expp1  9131  expnegap0  9132  expcllem  9135  mulexpzap  9164  expaddzap  9168  expmulzap  9170  shftf  9300  sqrtdiv  9509  mulcn2  9701  ialgrf  9752  bj-bdfindes  9938  bj-findes  9970
  Copyright terms: Public domain W3C validator