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  1311  19.30dc  1641  nf4r  1685  cbvexv1  1766  cbvexh  1769  equveli  1773  sbequilem  1852  sb5rf  1866  nfsbxy  1961  nfsbxyt  1962  sbcomxyyz  1991  dvelimALT  2029  dvelimfv  2030  dvelimor  2037  mo2n  2073  mo23  2086  2exeu  2137  bm1.1  2181  necon1idc  2420  sbhypf  2813  vtocl2  2819  vtocl3  2820  reu6  2953  rmo2ilem  3079  uneqin  3414  abn0r  3475  inelcm  3511  vdif0im  3516  difrab0eqim  3517  r19.3rm  3539  r19.9rmv  3542  difprsn1  3761  intminss  3899  disjnim  4024  bm1.3ii  4154  intexabim  4185  copsex2g  4279  opelopabt  4296  eusv2nf  4491  reusv3i  4494  onintrab2im  4554  ordtri2orexmid  4559  setindel  4574  onsucuni2  4600  ordtri2or2exmid  4607  zfregfr  4610  tfi  4618  mosubopt  4728  eqrelrel  4764  xpiindim  4803  opeliunxp2  4806  opelrn  4900  issref  5052  xpmlem  5090  rnxpid  5104  ssxpbm  5105  relcoi2  5200  unixpm  5205  cnviinm  5211  iotanul  5234  iotaexab  5237  funimaexglem  5341  fvelrnb  5608  fvmptssdm  5646  fnfvrnss  5722  fressnfv  5749  fconstfvm  5780  f1mpt  5818  ovprc  5957  fvmpopr2d  6059  fo1stresm  6219  fo2ndresm  6220  spc2ed  6291  opeliunxp2f  6296  reldmtpos  6311  tfrlem5  6372  tfrlem9  6377  tfri2  6424  frecfcllem  6462  frecsuclem  6464  fvmptmap  6744  ixpiinm  6783  ixp0  6790  mptelixpg  6793  ener  6838  domtr  6844  unen  6875  xpf1o  6905  mapen  6907  ss1o0el1o  6974  cardval3ex  7252  distrnqg  7454  nqnq0pi  7505  nqnq0a  7521  nqnq0m  7522  distrnq0  7526  nqprloc  7612  ltexprlemopl  7668  ltexprlemopu  7670  recexre  8605  nn1suc  9009  msqznn  9426  nn0ind  9440  fnn0ind  9442  ublbneg  9687  qreccl  9716  fzo1fzo0n0  10259  elfzom1elp1fzo  10278  fzo0end  10299  fzind2  10315  flqeqceilz  10410  nnsinds  10537  nn0sinds  10538  ser0f  10626  hashfacen  10928  iswrddm0  10959  redivap  11039  imdivap  11046  cvg1nlemres  11150  sqrt0  11169  summodclem3  11545  fsump1i  11598  prodf1  11707  cos1bnd  11924  odd2np1  12038  opoe  12060  omoe  12061  opeo  12062  omeo  12063  dfgcd2  12181  gcdmultiplez  12188  dvdssq  12198  algfx  12220  odzval  12410  mul4sq  12563  setsfun0  12714  rmodislmod  13907  isridl  14060  neipsm  14390  txbas  14494  elcncf1di  14815  plyco  14995  reeff1o  15009  sincosq1lem  15061  sincosq2sgn  15063  sincosq4sgn  15065  lgsne0  15279  2lgslem1  15332  mul2sq  15357  bdbm1.3ii  15537