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  1261  19.30dc  1589  nf4r  1632  cbvexh  1711  equveli  1715  sbequilem  1792  sb5rf  1806  nfsbxy  1893  nfsbxyt  1894  sbcomxyyz  1921  dvelimALT  1961  dvelimfv  1962  dvelimor  1969  mo2n  2003  mo23  2016  2exeu  2067  bm1.1  2100  necon1idc  2336  sbhypf  2707  vtocl2  2713  vtocl3  2714  reu6  2844  rmo2ilem  2968  uneqin  3295  abn0r  3355  inelcm  3391  vdif0im  3396  difrab0eqim  3397  r19.3rm  3419  r19.9rmv  3422  difprsn1  3627  intminss  3764  disjnim  3888  bm1.3ii  4017  intexabim  4045  copsex2g  4136  opelopabt  4152  eusv2nf  4345  reusv3i  4348  onintrab2im  4402  ordtri2orexmid  4406  setindel  4421  onsucuni2  4447  ordtri2or2exmid  4454  zfregfr  4456  tfi  4464  mosubopt  4572  eqrelrel  4608  xpiindim  4644  opeliunxp2  4647  opelrn  4741  issref  4889  xpmlem  4927  rnxpid  4941  ssxpbm  4942  relcoi2  5037  unixpm  5042  cnviinm  5048  iotanul  5071  funimaexglem  5174  fvelrnb  5435  fvmptssdm  5471  fnfvrnss  5546  fressnfv  5573  fconstfvm  5604  f1mpt  5638  ovprc  5772  fo1stresm  6025  fo2ndresm  6026  spc2ed  6096  opeliunxp2f  6101  reldmtpos  6116  tfrlem5  6177  tfrlem9  6182  tfri2  6229  frecfcllem  6267  frecsuclem  6269  fvmptmap  6545  ixpiinm  6584  ixp0  6591  mptelixpg  6594  ener  6639  domtr  6645  unen  6676  xpf1o  6704  mapen  6706  cardval3ex  7007  distrnqg  7159  nqnq0pi  7210  nqnq0a  7226  nqnq0m  7227  distrnq0  7231  nqprloc  7317  ltexprlemopl  7373  ltexprlemopu  7375  recexre  8303  nn1suc  8696  msqznn  9102  nn0ind  9116  fnn0ind  9118  ublbneg  9354  qreccl  9383  fzo1fzo0n0  9900  elfzom1elp1fzo  9919  fzo0end  9940  fzind2  9956  flqeqceilz  10031  nnsinds  10156  nn0sinds  10157  ser0f  10228  hashfacen  10519  redivap  10586  imdivap  10593  cvg1nlemres  10697  sqrt0  10716  summodclem3  11089  fsump1i  11142  cos1bnd  11365  odd2np1  11466  opoe  11488  omoe  11489  opeo  11490  omeo  11491  dfgcd2  11598  gcdmultiplez  11605  dvdssq  11615  algfx  11629  setsfun0  11890  neipsm  12218  txbas  12322  elcncf1di  12630  bdbm1.3ii  12891
  Copyright terms: Public domain W3C validator