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  6514  reldmtpos  6529  tfrlem5  6590  tfrlem9  6595  tfri2  6642  frecfcllem  6680  frecsuclem  6682  fvmptmap  6971  ixpiinm  7012  ixp0  7019  mptelixpg  7022  ener  7072  domtr  7078  unen  7111  xpf1o  7150  mapen  7152  ss1o0el1o  7226  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  9756  nn0ind  9770  fnn0ind  9772  ublbneg  10028  qreccl  10057  fzo1fzo0n0  10611  elfzom1elp1fzo  10636  fzo0end  10657  fzind2  10674  flqeqceilz  10775  nnsinds  10902  nn0sinds  10903  ser0f  10991  hashfacen  11305  iswrddm0  11349  swrdlsw  11462  pfxn0  11481  swrdswrdlem  11497  pfxccatin12lem3  11525  pfxccat3  11527  pfxccat3a  11531  swrdccat3blem  11532  redivap  11660  imdivap  11667  cvg1nlemres  11772  sqrt0  11791  summodclem3  12171  fsump1i  12224  prodf1  12333  cos1bnd  12550  odd2np1  12664  opoe  12686  omoe  12687  opeo  12688  omeo  12689  dfgcd2  12815  gcdmultiplez  12822  dvdssq  12832  algfx  12854  odzval  13048  mul4sq  13201  ballotfilemsdom  13312  ballotfilemth  13338  setsfun0  13445  rmodislmod  14796  isridl  14949  mvrclfi  15226  neipsm  15397  txbas  15501  elcncf1di  15822  plyco  16002  reeff1o  16016  sincosq1lem  16069  sincosq2sgn  16071  sincosq4sgn  16073  lgsne0  16379  2lgslem1  16432  mul2sq  16457  lpvtx  16542  umgrislfupgrenlem  16593  umgrislfupgrdom  16594  uspgr2wlkeq  16828  wlklenvclwlk  16836  bdbm1.3ii  17139  wexmiddiffilem  17265  wexmiddifxylem  17267  idjudju  17269  als-no-surprise  17371