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  1290  19.30dc  1615  nf4r  1659  cbvexv1  1740  cbvexh  1743  equveli  1747  sbequilem  1826  sb5rf  1840  nfsbxy  1930  nfsbxyt  1931  sbcomxyyz  1960  dvelimALT  1998  dvelimfv  1999  dvelimor  2006  mo2n  2042  mo23  2055  2exeu  2106  bm1.1  2150  necon1idc  2388  sbhypf  2774  vtocl2  2780  vtocl3  2781  reu6  2914  rmo2ilem  3039  uneqin  3372  abn0r  3432  inelcm  3468  vdif0im  3473  difrab0eqim  3474  r19.3rm  3496  r19.9rmv  3499  difprsn1  3711  intminss  3848  disjnim  3972  bm1.3ii  4102  intexabim  4130  copsex2g  4223  opelopabt  4239  eusv2nf  4433  reusv3i  4436  onintrab2im  4494  ordtri2orexmid  4499  setindel  4514  onsucuni2  4540  ordtri2or2exmid  4547  zfregfr  4550  tfi  4558  mosubopt  4668  eqrelrel  4704  xpiindim  4740  opeliunxp2  4743  opelrn  4837  issref  4985  xpmlem  5023  rnxpid  5037  ssxpbm  5038  relcoi2  5133  unixpm  5138  cnviinm  5144  iotanul  5167  funimaexglem  5270  fvelrnb  5533  fvmptssdm  5569  fnfvrnss  5644  fressnfv  5671  fconstfvm  5702  f1mpt  5738  ovprc  5873  fo1stresm  6126  fo2ndresm  6127  spc2ed  6197  opeliunxp2f  6202  reldmtpos  6217  tfrlem5  6278  tfrlem9  6283  tfri2  6330  frecfcllem  6368  frecsuclem  6370  fvmptmap  6647  ixpiinm  6686  ixp0  6693  mptelixpg  6696  ener  6741  domtr  6747  unen  6778  xpf1o  6806  mapen  6808  ss1o0el1o  6874  cardval3ex  7137  distrnqg  7324  nqnq0pi  7375  nqnq0a  7391  nqnq0m  7392  distrnq0  7396  nqprloc  7482  ltexprlemopl  7538  ltexprlemopu  7540  recexre  8472  nn1suc  8872  msqznn  9287  nn0ind  9301  fnn0ind  9303  ublbneg  9547  qreccl  9576  fzo1fzo0n0  10114  elfzom1elp1fzo  10133  fzo0end  10154  fzind2  10170  flqeqceilz  10249  nnsinds  10374  nn0sinds  10375  ser0f  10446  hashfacen  10745  redivap  10812  imdivap  10819  cvg1nlemres  10923  sqrt0  10942  summodclem3  11317  fsump1i  11370  prodf1  11479  cos1bnd  11696  odd2np1  11806  opoe  11828  omoe  11829  opeo  11830  omeo  11831  dfgcd2  11943  gcdmultiplez  11950  dvdssq  11960  algfx  11980  odzval  12169  mul4sq  12320  setsfun0  12426  neipsm  12754  txbas  12858  elcncf1di  13166  reeff1o  13294  sincosq1lem  13346  sincosq2sgn  13348  sincosq4sgn  13350  lgsne0  13539  mul2sq  13552  bdbm1.3ii  13733