Theorem sylbir 133

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

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

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  3imtr3i  198  3ori  1231  19.30dc  1558  nf4r  1601  cbvexh  1678  equveli  1682  sbequilem  1759  sb5rf  1773  nfsbxy  1859  nfsbxyt  1860  sbcomxyyz  1887  dvelimALT  1927  dvelimfv  1928  dvelimor  1935  mo2n  1969  mo23  1982  2exeu  2033  bm1.1  2066  necon1idc  2298  sbhypf  2648  vtocl2  2654  vtocl3  2655  reu6  2781  rmo2ilem  2903  uneqin  3215  abn0r  3270  inelcm  3304  vdif0im  3309  difrab0eqim  3310  r19.3rm  3330  r19.9rmv  3333  difprsn1  3525  intminss  3661  bm1.3ii  3899  intexabim  3927  copsex2g  4001  opelopabt  4017  eusv2nf  4206  reusv3i  4209  onintrab2im  4262  ordtri2orexmid  4266  setindel  4281  onsucuni2  4307  ordtri2or2exmid  4314  zfregfr  4316  tfi  4323  mosubopt  4423  eqrelrel  4459  xpiindim  4491  opeliunxp2  4494  opelrn  4586  issref  4727  xpmlem  4764  rnxpid  4775  ssxpbm  4776  relcoi2  4868  unixpm  4873  cnviinm  4879  iotanul  4902  funimaexglem  5002  fvelrnb  5242  fvmptssdm  5276  fnfvrnss  5346  fressnfv  5371  fconstfvm  5400  f1mpt  5431  ovprc  5560  fo1stresm  5808  fo2ndresm  5809  spc2ed  5874  reldmtpos  5891  tfrlem5  5953  tfrlem9  5958  tfri2  5975  ener  6282  domtr  6288  unen  6316  cardval3ex  6454  distrnqg  6577  nqnq0pi  6628  nqnq0a  6644  nqnq0m  6645  distrnq0  6649  nqprloc  6735  ltexprlemopl  6791  ltexprlemopu  6793  recexre  7678  nn1suc  8058  msqznn  8447  nn0ind  8461  fnn0ind  8463  ublbneg  8698  qreccl  8727  fzo1fzo0n0  9192  elfzom1elp1fzo  9211  fzo0end  9232  fzind2  9248  flqeqceilz  9320  nnsinds  9429  nn0sinds  9430  iser0f  9472  redivap  9761  imdivap  9768  cvg1nlemres  9871  sqrt0  9890  odd2np1  10272  opoe  10295  omoe  10296  opeo  10297  omeo  10298  dfgcd2  10403  gcdmultiplez  10410  dvdssq  10420  ialgfx  10434  bdbm1.3ii  10682