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

Theorem sylbir 133
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 131 . 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 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  3imtr3i  198  3ori  1236  19.30dc  1563  nf4r  1606  cbvexh  1685  equveli  1689  sbequilem  1766  sb5rf  1780  nfsbxy  1866  nfsbxyt  1867  sbcomxyyz  1894  dvelimALT  1934  dvelimfv  1935  dvelimor  1942  mo2n  1976  mo23  1989  2exeu  2040  bm1.1  2073  necon1idc  2308  sbhypf  2668  vtocl2  2674  vtocl3  2675  reu6  2802  rmo2ilem  2926  uneqin  3248  abn0r  3305  inelcm  3340  vdif0im  3345  difrab0eqim  3346  r19.3rm  3366  r19.9rmv  3369  difprsn1  3571  intminss  3708  disjnim  3828  bm1.3ii  3952  intexabim  3980  copsex2g  4064  opelopabt  4080  eusv2nf  4269  reusv3i  4272  onintrab2im  4325  ordtri2orexmid  4329  setindel  4344  onsucuni2  4370  ordtri2or2exmid  4377  zfregfr  4379  tfi  4387  mosubopt  4491  eqrelrel  4527  xpiindim  4561  opeliunxp2  4564  opelrn  4657  issref  4801  xpmlem  4839  rnxpid  4852  ssxpbm  4853  relcoi2  4948  unixpm  4953  cnviinm  4959  iotanul  4982  funimaexglem  5083  fvelrnb  5336  fvmptssdm  5371  fnfvrnss  5442  fressnfv  5468  fconstfvm  5497  f1mpt  5532  ovprc  5666  fo1stresm  5914  fo2ndresm  5915  spc2ed  5980  opeliunxp2f  5985  reldmtpos  6000  tfrlem5  6061  tfrlem9  6066  tfri2  6113  frecfcllem  6151  frecsuclem  6153  fvmptmap  6422  ener  6476  domtr  6482  unen  6513  xpf1o  6540  mapen  6542  cardval3ex  6792  distrnqg  6925  nqnq0pi  6976  nqnq0a  6992  nqnq0m  6993  distrnq0  6997  nqprloc  7083  ltexprlemopl  7139  ltexprlemopu  7141  recexre  8031  nn1suc  8413  msqznn  8816  nn0ind  8830  fnn0ind  8832  ublbneg  9067  qreccl  9096  fzo1fzo0n0  9559  elfzom1elp1fzo  9578  fzo0end  9599  fzind2  9615  flqeqceilz  9690  nnsinds  9814  nn0sinds  9815  iser0f  9913  ser0f  9915  hashfacen  10206  redivap  10273  imdivap  10280  cvg1nlemres  10383  sqrt0  10402  isummolem3  10734  fsump1i  10790  odd2np1  10966  opoe  10988  omoe  10989  opeo  10990  omeo  10991  dfgcd2  11096  gcdmultiplez  11103  dvdssq  11113  ialgfx  11127  bdbm1.3ii  11439
  Copyright terms: Public domain W3C validator