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  1278  19.30dc  1606  nf4r  1649  cbvexh  1728  equveli  1732  sbequilem  1810  sb5rf  1824  nfsbxy  1913  nfsbxyt  1914  sbcomxyyz  1943  dvelimALT  1983  dvelimfv  1984  dvelimor  1991  mo2n  2025  mo23  2038  2exeu  2089  bm1.1  2122  necon1idc  2359  sbhypf  2730  vtocl2  2736  vtocl3  2737  reu6  2868  rmo2ilem  2993  uneqin  3322  abn0r  3382  inelcm  3418  vdif0im  3423  difrab0eqim  3424  r19.3rm  3446  r19.9rmv  3449  difprsn1  3654  intminss  3791  disjnim  3915  bm1.3ii  4044  intexabim  4072  copsex2g  4163  opelopabt  4179  eusv2nf  4372  reusv3i  4375  onintrab2im  4429  ordtri2orexmid  4433  setindel  4448  onsucuni2  4474  ordtri2or2exmid  4481  zfregfr  4483  tfi  4491  mosubopt  4599  eqrelrel  4635  xpiindim  4671  opeliunxp2  4674  opelrn  4768  issref  4916  xpmlem  4954  rnxpid  4968  ssxpbm  4969  relcoi2  5064  unixpm  5069  cnviinm  5075  iotanul  5098  funimaexglem  5201  fvelrnb  5462  fvmptssdm  5498  fnfvrnss  5573  fressnfv  5600  fconstfvm  5631  f1mpt  5665  ovprc  5799  fo1stresm  6052  fo2ndresm  6053  spc2ed  6123  opeliunxp2f  6128  reldmtpos  6143  tfrlem5  6204  tfrlem9  6209  tfri2  6256  frecfcllem  6294  frecsuclem  6296  fvmptmap  6572  ixpiinm  6611  ixp0  6618  mptelixpg  6621  ener  6666  domtr  6672  unen  6703  xpf1o  6731  mapen  6733  cardval3ex  7034  distrnqg  7188  nqnq0pi  7239  nqnq0a  7255  nqnq0m  7256  distrnq0  7260  nqprloc  7346  ltexprlemopl  7402  ltexprlemopu  7404  recexre  8333  nn1suc  8732  msqznn  9144  nn0ind  9158  fnn0ind  9160  ublbneg  9398  qreccl  9427  fzo1fzo0n0  9953  elfzom1elp1fzo  9972  fzo0end  9993  fzind2  10009  flqeqceilz  10084  nnsinds  10209  nn0sinds  10210  ser0f  10281  hashfacen  10572  redivap  10639  imdivap  10646  cvg1nlemres  10750  sqrt0  10769  summodclem3  11142  fsump1i  11195  prodf1  11304  cos1bnd  11455  odd2np1  11559  opoe  11581  omoe  11582  opeo  11583  omeo  11584  dfgcd2  11691  gcdmultiplez  11698  dvdssq  11708  algfx  11722  setsfun0  11984  neipsm  12312  txbas  12416  elcncf1di  12724  sincosq1lem  12895  sincosq2sgn  12897  sincosq4sgn  12899  bdbm1.3ii  13078