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  1194  19.30dc  1515  nf4r  1558  cbvexh  1635  equveli  1639  sbequilem  1716  sb5rf  1729  nfsbxy  1815  nfsbxyt  1816  sbcomxyyz  1843  dvelimALT  1883  dvelimfv  1884  dvelimor  1891  mo2n  1925  mo23  1938  2exeu  1989  bm1.1  2022  necon1idc  2252  sbhypf  2597  vtocl2  2603  vtocl3  2604  reu6  2724  rmo2ilem  2841  uneqin  3182  abn0r  3237  inelcm  3276  vdif0im  3281  difrab0eqim  3282  r19.3rm  3304  r19.9rmv  3307  difprsn1  3494  intminss  3631  bm1.3ii  3869  intexabim  3897  copsex2g  3974  opelopabt  3990  eusv2nf  4154  reusv3i  4157  ordtri2orexmid  4211  setindel  4221  tfi  4248  mosubopt  4348  eqrelrel  4384  xpiindim  4416  opeliunxp2  4419  opelrn  4511  issref  4650  xpmlem  4687  rnxpid  4698  ssxpbm  4699  relcoi2  4791  unixpm  4796  cnviinm  4802  iotanul  4825  funimaexglem  4925  fvelrnb  5164  fvmptssdm  5198  fnfvrnss  5268  fressnfv  5293  fconstfvm  5322  f1mpt  5353  ovprc  5482  fo1stresm  5730  fo2ndresm  5731  reldmtpos  5809  tfrlem5  5871  tfrlem9  5876  tfri2  5893  ener  6195  domtr  6201  unen  6229  distrnqg  6371  nqnq0pi  6421  nqnq0a  6437  nqnq0m  6438  distrnq0  6442  nqprloc  6528  ltexprlemopl  6575  ltexprlemopu  6577  recexre  7362  nn1suc  7714  msqznn  8114  nn0ind  8128  fnn0ind  8130  ublbneg  8324  qreccl  8351  fzo1fzo0n0  8809  elfzom1elp1fzo  8828  fzo0end  8849  fzind2  8865  redivap  9102  imdivap  9109  sqrt0  9213  bdbm1.3ii  9346