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

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

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  1279  19.30dc  1607  nf4r  1650  cbvexh  1729  equveli  1733  sbequilem  1811  sb5rf  1825  nfsbxy  1916  nfsbxyt  1917  sbcomxyyz  1946  dvelimALT  1986  dvelimfv  1987  dvelimor  1994  mo2n  2028  mo23  2041  2exeu  2092  bm1.1  2125  necon1idc  2362  sbhypf  2738  vtocl2  2744  vtocl3  2745  reu6  2877  rmo2ilem  3002  uneqin  3332  abn0r  3392  inelcm  3428  vdif0im  3433  difrab0eqim  3434  r19.3rm  3456  r19.9rmv  3459  difprsn1  3667  intminss  3804  disjnim  3928  bm1.3ii  4057  intexabim  4085  copsex2g  4176  opelopabt  4192  eusv2nf  4385  reusv3i  4388  onintrab2im  4442  ordtri2orexmid  4446  setindel  4461  onsucuni2  4487  ordtri2or2exmid  4494  zfregfr  4496  tfi  4504  mosubopt  4612  eqrelrel  4648  xpiindim  4684  opeliunxp2  4687  opelrn  4781  issref  4929  xpmlem  4967  rnxpid  4981  ssxpbm  4982  relcoi2  5077  unixpm  5082  cnviinm  5088  iotanul  5111  funimaexglem  5214  fvelrnb  5477  fvmptssdm  5513  fnfvrnss  5588  fressnfv  5615  fconstfvm  5646  f1mpt  5680  ovprc  5814  fo1stresm  6067  fo2ndresm  6068  spc2ed  6138  opeliunxp2f  6143  reldmtpos  6158  tfrlem5  6219  tfrlem9  6224  tfri2  6271  frecfcllem  6309  frecsuclem  6311  fvmptmap  6587  ixpiinm  6626  ixp0  6633  mptelixpg  6636  ener  6681  domtr  6687  unen  6718  xpf1o  6746  mapen  6748  cardval3ex  7058  distrnqg  7219  nqnq0pi  7270  nqnq0a  7286  nqnq0m  7287  distrnq0  7291  nqprloc  7377  ltexprlemopl  7433  ltexprlemopu  7435  recexre  8364  nn1suc  8763  msqznn  9175  nn0ind  9189  fnn0ind  9191  ublbneg  9432  qreccl  9461  fzo1fzo0n0  9991  elfzom1elp1fzo  10010  fzo0end  10031  fzind2  10047  flqeqceilz  10122  nnsinds  10247  nn0sinds  10248  ser0f  10319  hashfacen  10611  redivap  10678  imdivap  10685  cvg1nlemres  10789  sqrt0  10808  summodclem3  11181  fsump1i  11234  prodf1  11343  cos1bnd  11502  odd2np1  11606  opoe  11628  omoe  11629  opeo  11630  omeo  11631  dfgcd2  11738  gcdmultiplez  11745  dvdssq  11755  algfx  11769  setsfun0  12034  neipsm  12362  txbas  12466  elcncf1di  12774  reeff1o  12902  sincosq1lem  12954  sincosq2sgn  12956  sincosq4sgn  12958  bdbm1.3ii  13260