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

Theorem sylbir 134
Description: A mixed syllogism inference from a biconditional and an implication. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
sylbir.1  |-  ( ps  <->  ph )
sylbir.2  |-  ( ps 
->  ch )
Assertion
Ref Expression
sylbir  |-  ( ph  ->  ch )

Proof of Theorem sylbir
StepHypRef Expression
1 sylbir.1 . . 3  |-  ( ps  <->  ph )
21biimpri 132 . 2  |-  ( ph  ->  ps )
3 sylbir.2 . 2  |-  ( ps 
->  ch )
42, 3syl 14 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> 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:  3imtr3i  199  3ori  1263  19.30dc  1591  nf4r  1634  cbvexh  1713  equveli  1717  sbequilem  1794  sb5rf  1808  nfsbxy  1895  nfsbxyt  1896  sbcomxyyz  1923  dvelimALT  1963  dvelimfv  1964  dvelimor  1971  mo2n  2005  mo23  2018  2exeu  2069  bm1.1  2102  necon1idc  2338  sbhypf  2709  vtocl2  2715  vtocl3  2716  reu6  2846  rmo2ilem  2970  uneqin  3297  abn0r  3357  inelcm  3393  vdif0im  3398  difrab0eqim  3399  r19.3rm  3421  r19.9rmv  3424  difprsn1  3629  intminss  3766  disjnim  3890  bm1.3ii  4019  intexabim  4047  copsex2g  4138  opelopabt  4154  eusv2nf  4347  reusv3i  4350  onintrab2im  4404  ordtri2orexmid  4408  setindel  4423  onsucuni2  4449  ordtri2or2exmid  4456  zfregfr  4458  tfi  4466  mosubopt  4574  eqrelrel  4610  xpiindim  4646  opeliunxp2  4649  opelrn  4743  issref  4891  xpmlem  4929  rnxpid  4943  ssxpbm  4944  relcoi2  5039  unixpm  5044  cnviinm  5050  iotanul  5073  funimaexglem  5176  fvelrnb  5437  fvmptssdm  5473  fnfvrnss  5548  fressnfv  5575  fconstfvm  5606  f1mpt  5640  ovprc  5774  fo1stresm  6027  fo2ndresm  6028  spc2ed  6098  opeliunxp2f  6103  reldmtpos  6118  tfrlem5  6179  tfrlem9  6184  tfri2  6231  frecfcllem  6269  frecsuclem  6271  fvmptmap  6547  ixpiinm  6586  ixp0  6593  mptelixpg  6596  ener  6641  domtr  6647  unen  6678  xpf1o  6706  mapen  6708  cardval3ex  7009  distrnqg  7163  nqnq0pi  7214  nqnq0a  7230  nqnq0m  7231  distrnq0  7235  nqprloc  7321  ltexprlemopl  7377  ltexprlemopu  7379  recexre  8307  nn1suc  8703  msqznn  9109  nn0ind  9123  fnn0ind  9125  ublbneg  9361  qreccl  9390  fzo1fzo0n0  9915  elfzom1elp1fzo  9934  fzo0end  9955  fzind2  9971  flqeqceilz  10046  nnsinds  10171  nn0sinds  10172  ser0f  10243  hashfacen  10534  redivap  10601  imdivap  10608  cvg1nlemres  10712  sqrt0  10731  summodclem3  11104  fsump1i  11157  cos1bnd  11380  odd2np1  11482  opoe  11504  omoe  11505  opeo  11506  omeo  11507  dfgcd2  11614  gcdmultiplez  11621  dvdssq  11631  algfx  11645  setsfun0  11906  neipsm  12234  txbas  12338  elcncf1di  12646  sincosq1lem  12817  sincosq2sgn  12819  sincosq4sgn  12821  bdbm1.3ii  12985
  Copyright terms: Public domain W3C validator