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

Theorem sylan2b 275
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 117 . 2  |-  ( ph  ->  ch )
3 sylan2b.2 . 2  |-  ( ( ps  /\  ch )  ->  th )
42, 3sylan2 274 1  |-  ( ( ps  /\  ph )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101    <-> wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  syl2anb  279  dcor  854  bm1.1  2041  eqtr3  2075  morex  2747  reuss2  3244  reupick  3248  rabsneu  3470  opabss  3848  triun  3894  poirr  4071  wepo  4123  wetrep  4124  rexxfrd  4222  reg3exmidlemwe  4330  nnsuc  4365  fnfco  5092  fun11iun  5174  fnressn  5376  fvpr1g  5394  fvtp1g  5396  fvtp3g  5398  fvtp3  5401  f1mpt  5437  caovlem2d  5720  offval  5746  dfoprab3  5844  1stconst  5869  2ndconst  5870  poxp  5880  tfrlemisucaccv  5969  addclpi  6482  addnidpig  6491  reapmul1  7659  nnnn0addcl  8268  un0addcl  8271  un0mulcl  8272  zltnle  8347  nn0ge0div  8384  uzind3  8409  uzind4  8626  ltsubrp  8714  ltaddrp  8715  xrlttr  8816  xrltso  8817  xltnegi  8848  fzind2  9196  qltnle  9202  qbtwnxr  9213  expp1  9426  expnegap0  9427  expcllem  9430  mulexpzap  9459  expaddzap  9463  expmulzap  9465  shftf  9658  sqrtdiv  9868  mulcn2  10063  dvdsflip  10162  dvdsfac  10171  ialgrf  10246  bj-bdfindes  10440  bj-findes  10472
  Copyright terms: Public domain W3C validator