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

Theorem sylan2b 285
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 284 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-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  syl2anb  289  dcor  904  bm1.1  2102  eqtr3  2137  elnelne1  2389  elnelne2  2390  morex  2841  reuss2  3326  reupick  3330  rabsneu  3566  opabss  3962  triun  4009  poirr  4199  wepo  4251  wetrep  4252  rexxfrd  4354  reg3exmidlemwe  4463  nnsuc  4499  fnfco  5267  fun11iun  5356  fnressn  5574  fvpr1g  5594  fvtp1g  5596  fvtp3g  5598  fvtp3  5601  f1mpt  5640  caovlem2d  5931  offval  5957  dfoprab3  6057  1stconst  6086  2ndconst  6087  poxp  6097  tfrlemisucaccv  6190  tfr1onlemsucaccv  6206  tfrcllemsucaccv  6219  fiintim  6785  addclpi  7103  addnidpig  7112  reapmul1  8325  nnnn0addcl  8975  un0addcl  8978  un0mulcl  8979  zltnle  9068  nn0ge0div  9106  uzind3  9132  uzind4  9351  ltsubrp  9446  ltaddrp  9447  xrlttr  9549  xrltso  9550  xltnegi  9586  xaddnemnf  9608  xaddnepnf  9609  xaddcom  9612  xnegdi  9619  xsubge0  9632  fzind2  9984  qltnle  9991  qbtwnxr  10003  exp3vallem  10262  expp1  10268  expnegap0  10269  expcllem  10272  mulexpzap  10301  expaddzap  10305  expmulzap  10307  hashunlem  10518  shftf  10570  sqrtdiv  10782  mulcn2  11049  summodclem2  11119  fsum3  11124  cvgratz  11269  dvdsflip  11476  dvdsfac  11485  lcmgcdlem  11685  rpexp1i  11759  hashdvds  11824  hashgcdlem  11830  lmss  12342  xmetrtri  12472  blssioo  12641  divcnap  12651  dedekindicc  12707  dvidlemap  12756  dvrecap  12773  dveflem  12782  bj-bdfindes  13074  bj-findes  13106
  Copyright terms: Public domain W3C validator