Theorem sylbir 125

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

Step	Hyp	Ref	Expression
1		sylbir.1	. . 3 |- ( ps <-> ph )
2	1	biimpri 124	. 2 |- ( ph -> ps )
3		sylbir.2	. 2 |- ( ps -> ch )
4	2, 3	syl 14	1 |- ( ph -> ch )

Syntax hints:   -> wi 4   <-> wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  3imtr3i  189  3ori  1195  19.30dc  1518  nf4r  1561  cbvexh  1638  equveli  1642  sbequilem  1719  sb5rf  1732  nfsbxy  1818  nfsbxyt  1819  sbcomxyyz  1846  dvelimALT  1886  dvelimfv  1887  dvelimor  1894  mo2n  1928  mo23  1941  2exeu  1992  bm1.1  2025  necon1idc  2258  sbhypf  2603  vtocl2  2609  vtocl3  2610  reu6  2730  rmo2ilem  2847  uneqin  3188  abn0r  3243  inelcm  3282  vdif0im  3287  difrab0eqim  3288  r19.3rm  3310  r19.9rmv  3313  difprsn1  3503  intminss  3640  bm1.3ii  3878  intexabim  3906  copsex2g  3983  opelopabt  3999  eusv2nf  4188  reusv3i  4191  onintrab2im  4244  ordtri2orexmid  4248  setindel  4263  onsucuni2  4288  ordtri2or2exmid  4296  zfregfr  4298  tfi  4305  mosubopt  4405  eqrelrel  4441  xpiindim  4473  opeliunxp2  4476  opelrn  4568  issref  4707  xpmlem  4744  rnxpid  4755  ssxpbm  4756  relcoi2  4848  unixpm  4853  cnviinm  4859  iotanul  4882  funimaexglem  4982  fvelrnb  5221  fvmptssdm  5255  fnfvrnss  5325  fressnfv  5350  fconstfvm  5379  f1mpt  5410  ovprc  5540  fo1stresm  5788  fo2ndresm  5789  reldmtpos  5868  tfrlem5  5930  tfrlem9  5935  tfri2  5952  ener  6259  domtr  6265  unen  6293  cardval3ex  6365  distrnqg  6485  nqnq0pi  6536  nqnq0a  6552  nqnq0m  6553  distrnq0  6557  nqprloc  6643  ltexprlemopl  6699  ltexprlemopu  6701  recexre  7569  nn1suc  7933  msqznn  8338  nn0ind  8352  fnn0ind  8354  ublbneg  8548  qreccl  8576  fzo1fzo0n0  9039  elfzom1elp1fzo  9058  fzo0end  9079  fzind2  9095  flqeqceilz  9160  iser0f  9251  redivap  9474  imdivap  9481  cvg1nlemres  9584  sqrt0  9602  ialgfx  9891  bdbm1.3ii  10011