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 )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  3imtr3i  200  3ori  1341  19.30dc  1680  nf4r  1723  cbvexv1  1805  cbvexh  1808  equveli  1812  sbequilem  1891  sb5rf  1905  nfsbxy  2002  nfsbxyt  2003  sbcomxyyz  2032  dvelimALT  2070  dvelimfv  2071  dvelimor  2078  mo2n  2114  mo23  2128  2exeu  2179  bm1.1  2223  necon1idc  2473  sbhypf  2872  vtocl2  2878  vtocl3  2879  reu6  3015  rmo2ilem  3142  rabssrabd  3335  uneqin  3482  abn0r  3546  inelcm  3585  vdif0im  3590  difrab0eqim  3591  r19.3rm  3616  r19.9rmv  3619  difprsn1  3854  intminss  3995  disjnim  4120  bm1.3ii  4256  intexabim  4290  copsex2g  4388  opelopabt  4406  eusv2nf  4604  reusv3i  4607  onintrab2im  4667  ordtri2orexmid  4672  setindel  4687  onsucuni2  4713  ordtri2or2exmid  4720  zfregfr  4723  tfi  4731  mosubopt  4842  eqrelrel  4878  xpiindim  4919  opeliunxp2  4922  opelrn  5018  issref  5173  xpmlem  5211  rnxpid  5225  ssxpbm  5226  relcoi2  5321  unixpm  5326  cnviinm  5332  iotanul  5356  iotaexab  5359  funimaexglem  5467  fvelrnb  5753  fvmptssdm  5793  fnfvrnss  5871  fressnfv  5905  fconstfvm  5936  f1mpt  5980  ovprc  6124  fvmpopr2d  6228  fo1stresm  6399  fo2ndresm  6400  spc2ed  6473  opeliunxp2f  6513  reldmtpos  6528  tfrlem5  6589  tfrlem9  6594  tfri2  6641  frecfcllem  6679  frecsuclem  6681  fvmptmap  6970  ixpiinm  7010  ixp0  7017  mptelixpg  7020  ener  7070  domtr  7076  unen  7109  xpf1o  7148  mapen  7150  ss1o0el1o  7224  cardval3ex  7536  pr2cv2  7548  distrnqg  7760  nqnq0pi  7811  nqnq0a  7827  nqnq0m  7828  distrnq0  7832  nqprloc  7918  ltexprlemopl  7974  ltexprlemopu  7976  recexre  8914  nn1suc  9332  msqznn  9757  nn0ind  9771  fnn0ind  9773  ublbneg  10029  qreccl  10058  fzo1fzo0n0  10612  elfzom1elp1fzo  10637  fzo0end  10658  fzind2  10675  flqeqceilz  10776  nnsinds  10903  nn0sinds  10904  ser0f  10992  hashfacen  11306  iswrddm0  11350  swrdlsw  11463  pfxn0  11482  swrdswrdlem  11498  pfxccatin12lem3  11526  pfxccat3  11528  pfxccat3a  11532  swrdccat3blem  11533  redivap  11661  imdivap  11668  cvg1nlemres  11773  sqrt0  11792  summodclem3  12172  fsump1i  12225  prodf1  12334  cos1bnd  12551  odd2np1  12665  opoe  12687  omoe  12688  opeo  12689  omeo  12690  dfgcd2  12816  gcdmultiplez  12823  dvdssq  12833  algfx  12855  odzval  13049  mul4sq  13202  ballotfilemsdom  13313  ballotfilemth  13339  setsfun0  13446  rmodislmod  14797  isridl  14950  neipsm  15380  txbas  15484  elcncf1di  15805  plyco  15985  reeff1o  15999  sincosq1lem  16052  sincosq2sgn  16054  sincosq4sgn  16056  lgsne0  16362  2lgslem1  16415  mul2sq  16440  lpvtx  16525  umgrislfupgrenlem  16576  umgrislfupgrdom  16577  uspgr2wlkeq  16811  wlklenvclwlk  16819  bdbm1.3ii  17122  wexmiddiffilem  17248  wexmiddifxylem  17250  idjudju  17252  als-no-surprise  17354