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

Theorem sylan2b 287
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 120 . 2  |-  ( ph  ->  ch )
3 sylan2b.2 . 2  |-  ( ( ps  /\  ch )  ->  th )
42, 3sylan2 286 1  |-  ( ( ps  /\  ph )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    <-> wb 105
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
This theorem is referenced by:  syl2anb  291  dcor  935  bm1.1  2162  eqtr3  2197  elnelne1  2451  elnelne2  2452  morex  2921  reuss2  3415  reupick  3419  rabsneu  3664  opabss  4064  triun  4111  poirr  4303  wepo  4355  wetrep  4356  rexxfrd  4459  reg3exmidlemwe  4574  nnsuc  4611  fnfco  5385  fun11iun  5477  fnressn  5697  fvpr1g  5717  fvtp1g  5719  fvtp3g  5721  fvtp3  5724  f1mpt  5765  caovlem2d  6060  offval  6083  dfoprab3  6185  1stconst  6215  2ndconst  6216  poxp  6226  tfrlemisucaccv  6319  tfr1onlemsucaccv  6335  tfrcllemsucaccv  6348  fiintim  6921  addclpi  7304  addnidpig  7313  reapmul1  8529  nnnn0addcl  9182  un0addcl  9185  un0mulcl  9186  zltnle  9275  nn0ge0div  9316  uzind3  9342  uzind4  9564  ltsubrp  9664  ltaddrp  9665  xrlttr  9769  xrltso  9770  xltnegi  9809  xaddnemnf  9831  xaddnepnf  9832  xaddcom  9835  xnegdi  9842  xsubge0  9855  fzind2  10212  qltnle  10219  qbtwnxr  10231  exp3vallem  10494  expp1  10500  expnegap0  10501  expcllem  10504  mulexpzap  10533  expaddzap  10537  expmulzap  10539  hashunlem  10755  shftf  10810  sqrtdiv  11022  mulcn2  11291  summodclem2  11361  fsum3  11366  cvgratz  11511  prodmodclem2  11556  zproddc  11558  prodsnf  11571  dvdsflip  11827  dvdsfac  11836  lcmgcdlem  12047  rpexp1i  12124  hashdvds  12191  hashgcdlem  12208  phisum  12210  pcqcl  12276  pcid  12293  ssnnctlemct  12417  issubmd  12742  grpinvnzcl  12818  mulgneg  12877  mulgnn0z  12885  lmss  13379  xmetrtri  13509  blssioo  13678  divcnap  13688  dedekindicc  13744  dvidlemap  13793  dvrecap  13810  dveflem  13820  lgsval3  14052  lgsdir2  14067  2sqlem6  14089  bj-bdfindes  14323  bj-findes  14355
  Copyright terms: Public domain W3C validator