Theorem sylbir 135

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 133	. 2 |- ( ph -> ps )
3		sylbir.2	. 2 |- ( ps -> ch )
4	2, 3	syl 14	1 |- ( ph -> ch )

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  3imtr3i  200  3ori  1300  19.30dc  1627  nf4r  1671  cbvexv1  1752  cbvexh  1755  equveli  1759  sbequilem  1838  sb5rf  1852  nfsbxy  1942  nfsbxyt  1943  sbcomxyyz  1972  dvelimALT  2010  dvelimfv  2011  dvelimor  2018  mo2n  2054  mo23  2067  2exeu  2118  bm1.1  2162  necon1idc  2400  sbhypf  2788  vtocl2  2794  vtocl3  2795  reu6  2928  rmo2ilem  3054  uneqin  3388  abn0r  3449  inelcm  3485  vdif0im  3490  difrab0eqim  3491  r19.3rm  3513  r19.9rmv  3516  difprsn1  3733  intminss  3871  disjnim  3996  bm1.3ii  4126  intexabim  4154  copsex2g  4248  opelopabt  4264  eusv2nf  4458  reusv3i  4461  onintrab2im  4519  ordtri2orexmid  4524  setindel  4539  onsucuni2  4565  ordtri2or2exmid  4572  zfregfr  4575  tfi  4583  mosubopt  4693  eqrelrel  4729  xpiindim  4766  opeliunxp2  4769  opelrn  4863  issref  5013  xpmlem  5051  rnxpid  5065  ssxpbm  5066  relcoi2  5161  unixpm  5166  cnviinm  5172  iotanul  5195  funimaexglem  5301  fvelrnb  5565  fvmptssdm  5602  fnfvrnss  5678  fressnfv  5705  fconstfvm  5736  f1mpt  5774  ovprc  5912  fo1stresm  6164  fo2ndresm  6165  spc2ed  6236  opeliunxp2f  6241  reldmtpos  6256  tfrlem5  6317  tfrlem9  6322  tfri2  6369  frecfcllem  6407  frecsuclem  6409  fvmptmap  6687  ixpiinm  6726  ixp0  6733  mptelixpg  6736  ener  6781  domtr  6787  unen  6818  xpf1o  6846  mapen  6848  ss1o0el1o  6914  cardval3ex  7186  distrnqg  7388  nqnq0pi  7439  nqnq0a  7455  nqnq0m  7456  distrnq0  7460  nqprloc  7546  ltexprlemopl  7602  ltexprlemopu  7604  recexre  8537  nn1suc  8940  msqznn  9355  nn0ind  9369  fnn0ind  9371  ublbneg  9615  qreccl  9644  fzo1fzo0n0  10185  elfzom1elp1fzo  10204  fzo0end  10225  fzind2  10241  flqeqceilz  10320  nnsinds  10445  nn0sinds  10446  ser0f  10517  hashfacen  10818  redivap  10885  imdivap  10892  cvg1nlemres  10996  sqrt0  11015  summodclem3  11390  fsump1i  11443  prodf1  11552  cos1bnd  11769  odd2np1  11880  opoe  11902  omoe  11903  opeo  11904  omeo  11905  dfgcd2  12017  gcdmultiplez  12024  dvdssq  12034  algfx  12054  odzval  12243  mul4sq  12394  setsfun0  12500  rmodislmod  13446  neipsm  13693  txbas  13797  elcncf1di  14105  reeff1o  14233  sincosq1lem  14285  sincosq2sgn  14287  sincosq4sgn  14289  lgsne0  14478  mul2sq  14502  bdbm1.3ii  14682