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  1313  19.30dc  1651  nf4r  1695  cbvexv1  1776  cbvexh  1779  equveli  1783  sbequilem  1862  sb5rf  1876  nfsbxy  1971  nfsbxyt  1972  sbcomxyyz  2001  dvelimALT  2039  dvelimfv  2040  dvelimor  2047  mo2n  2083  mo23  2097  2exeu  2148  bm1.1  2192  necon1idc  2431  sbhypf  2827  vtocl2  2833  vtocl3  2834  reu6  2969  rmo2ilem  3096  uneqin  3432  abn0r  3493  inelcm  3529  vdif0im  3534  difrab0eqim  3535  r19.3rm  3557  r19.9rmv  3560  difprsn1  3783  intminss  3924  disjnim  4049  bm1.3ii  4181  intexabim  4212  copsex2g  4308  opelopabt  4326  eusv2nf  4521  reusv3i  4524  onintrab2im  4584  ordtri2orexmid  4589  setindel  4604  onsucuni2  4630  ordtri2or2exmid  4637  zfregfr  4640  tfi  4648  mosubopt  4758  eqrelrel  4794  xpiindim  4833  opeliunxp2  4836  opelrn  4931  issref  5084  xpmlem  5122  rnxpid  5136  ssxpbm  5137  relcoi2  5232  unixpm  5237  cnviinm  5243  iotanul  5266  iotaexab  5269  funimaexglem  5376  fvelrnb  5649  fvmptssdm  5687  fnfvrnss  5763  fressnfv  5794  fconstfvm  5825  f1mpt  5863  ovprc  6003  fvmpopr2d  6105  fo1stresm  6270  fo2ndresm  6271  spc2ed  6342  opeliunxp2f  6347  reldmtpos  6362  tfrlem5  6423  tfrlem9  6428  tfri2  6475  frecfcllem  6513  frecsuclem  6515  fvmptmap  6795  ixpiinm  6834  ixp0  6841  mptelixpg  6844  ener  6894  domtr  6900  unen  6932  xpf1o  6966  mapen  6968  ss1o0el1o  7036  cardval3ex  7318  pr2cv2  7330  distrnqg  7535  nqnq0pi  7586  nqnq0a  7602  nqnq0m  7603  distrnq0  7607  nqprloc  7693  ltexprlemopl  7749  ltexprlemopu  7751  recexre  8686  nn1suc  9090  msqznn  9508  nn0ind  9522  fnn0ind  9524  ublbneg  9769  qreccl  9798  fzo1fzo0n0  10344  elfzom1elp1fzo  10368  fzo0end  10389  fzind2  10405  flqeqceilz  10500  nnsinds  10627  nn0sinds  10628  ser0f  10716  hashfacen  11018  iswrddm0  11055  swrdlsw  11160  pfxn0  11179  swrdswrdlem  11195  pfxccatin12lem3  11223  pfxccat3  11225  pfxccat3a  11229  swrdccat3blem  11230  redivap  11300  imdivap  11307  cvg1nlemres  11411  sqrt0  11430  summodclem3  11806  fsump1i  11859  prodf1  11968  cos1bnd  12185  odd2np1  12299  opoe  12321  omoe  12322  opeo  12323  omeo  12324  dfgcd2  12450  gcdmultiplez  12457  dvdssq  12467  algfx  12489  odzval  12679  mul4sq  12832  setsfun0  12983  rmodislmod  14228  isridl  14381  neipsm  14741  txbas  14845  elcncf1di  15166  plyco  15346  reeff1o  15360  sincosq1lem  15412  sincosq2sgn  15414  sincosq4sgn  15416  lgsne0  15630  2lgslem1  15683  mul2sq  15708  lpvtx  15790  umgrislfupgrenlem  15836  umgrislfupgrdom  15837  bdbm1.3ii  16026