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  1295  19.30dc  1620  nf4r  1664  cbvexv1  1745  cbvexh  1748  equveli  1752  sbequilem  1831  sb5rf  1845  nfsbxy  1935  nfsbxyt  1936  sbcomxyyz  1965  dvelimALT  2003  dvelimfv  2004  dvelimor  2011  mo2n  2047  mo23  2060  2exeu  2111  bm1.1  2155  necon1idc  2393  sbhypf  2779  vtocl2  2785  vtocl3  2786  reu6  2919  rmo2ilem  3044  uneqin  3378  abn0r  3439  inelcm  3475  vdif0im  3480  difrab0eqim  3481  r19.3rm  3503  r19.9rmv  3506  difprsn1  3719  intminss  3856  disjnim  3980  bm1.3ii  4110  intexabim  4138  copsex2g  4231  opelopabt  4247  eusv2nf  4441  reusv3i  4444  onintrab2im  4502  ordtri2orexmid  4507  setindel  4522  onsucuni2  4548  ordtri2or2exmid  4555  zfregfr  4558  tfi  4566  mosubopt  4676  eqrelrel  4712  xpiindim  4748  opeliunxp2  4751  opelrn  4845  issref  4993  xpmlem  5031  rnxpid  5045  ssxpbm  5046  relcoi2  5141  unixpm  5146  cnviinm  5152  iotanul  5175  funimaexglem  5281  fvelrnb  5544  fvmptssdm  5580  fnfvrnss  5656  fressnfv  5683  fconstfvm  5714  f1mpt  5750  ovprc  5888  fo1stresm  6140  fo2ndresm  6141  spc2ed  6212  opeliunxp2f  6217  reldmtpos  6232  tfrlem5  6293  tfrlem9  6298  tfri2  6345  frecfcllem  6383  frecsuclem  6385  fvmptmap  6663  ixpiinm  6702  ixp0  6709  mptelixpg  6712  ener  6757  domtr  6763  unen  6794  xpf1o  6822  mapen  6824  ss1o0el1o  6890  cardval3ex  7162  distrnqg  7349  nqnq0pi  7400  nqnq0a  7416  nqnq0m  7417  distrnq0  7421  nqprloc  7507  ltexprlemopl  7563  ltexprlemopu  7565  recexre  8497  nn1suc  8897  msqznn  9312  nn0ind  9326  fnn0ind  9328  ublbneg  9572  qreccl  9601  fzo1fzo0n0  10139  elfzom1elp1fzo  10158  fzo0end  10179  fzind2  10195  flqeqceilz  10274  nnsinds  10399  nn0sinds  10400  ser0f  10471  hashfacen  10771  redivap  10838  imdivap  10845  cvg1nlemres  10949  sqrt0  10968  summodclem3  11343  fsump1i  11396  prodf1  11505  cos1bnd  11722  odd2np1  11832  opoe  11854  omoe  11855  opeo  11856  omeo  11857  dfgcd2  11969  gcdmultiplez  11976  dvdssq  11986  algfx  12006  odzval  12195  mul4sq  12346  setsfun0  12452  neipsm  12948  txbas  13052  elcncf1di  13360  reeff1o  13488  sincosq1lem  13540  sincosq2sgn  13542  sincosq4sgn  13544  lgsne0  13733  mul2sq  13746  bdbm1.3ii  13926