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 )

Syntax hints:   -> wi 4   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  3imtr3i  200  3ori  1337  19.30dc  1676  nf4r  1719  cbvexv1  1800  cbvexh  1803  equveli  1807  sbequilem  1886  sb5rf  1900  nfsbxy  1995  nfsbxyt  1996  sbcomxyyz  2025  dvelimALT  2063  dvelimfv  2064  dvelimor  2071  mo2n  2107  mo23  2121  2exeu  2172  bm1.1  2216  necon1idc  2456  sbhypf  2854  vtocl2  2860  vtocl3  2861  reu6  2996  rmo2ilem  3123  rabssrabd  3315  uneqin  3460  abn0r  3521  inelcm  3557  vdif0im  3562  difrab0eqim  3563  r19.3rm  3585  r19.9rmv  3588  difprsn1  3817  intminss  3958  disjnim  4083  bm1.3ii  4215  intexabim  4247  copsex2g  4344  opelopabt  4362  eusv2nf  4559  reusv3i  4562  onintrab2im  4622  ordtri2orexmid  4627  setindel  4642  onsucuni2  4668  ordtri2or2exmid  4675  zfregfr  4678  tfi  4686  mosubopt  4797  eqrelrel  4833  xpiindim  4873  opeliunxp2  4876  opelrn  4972  issref  5126  xpmlem  5164  rnxpid  5178  ssxpbm  5179  relcoi2  5274  unixpm  5279  cnviinm  5285  iotanul  5309  iotaexab  5312  funimaexglem  5420  fvelrnb  5702  fvmptssdm  5740  fnfvrnss  5815  fressnfv  5849  fconstfvm  5880  f1mpt  5922  ovprc  6064  fvmpopr2d  6168  fo1stresm  6333  fo2ndresm  6334  spc2ed  6407  opeliunxp2f  6447  reldmtpos  6462  tfrlem5  6523  tfrlem9  6528  tfri2  6575  frecfcllem  6613  frecsuclem  6615  fvmptmap  6897  ixpiinm  6936  ixp0  6943  mptelixpg  6946  ener  6996  domtr  7002  unen  7034  xpf1o  7073  mapen  7075  ss1o0el1o  7148  cardval3ex  7449  pr2cv2  7461  distrnqg  7667  nqnq0pi  7718  nqnq0a  7734  nqnq0m  7735  distrnq0  7739  nqprloc  7825  ltexprlemopl  7881  ltexprlemopu  7883  recexre  8817  nn1suc  9221  msqznn  9641  nn0ind  9655  fnn0ind  9657  ublbneg  9908  qreccl  9937  fzo1fzo0n0  10485  elfzom1elp1fzo  10510  fzo0end  10531  fzind2  10548  flqeqceilz  10643  nnsinds  10770  nn0sinds  10771  ser0f  10859  hashfacen  11163  iswrddm0  11203  swrdlsw  11316  pfxn0  11335  swrdswrdlem  11351  pfxccatin12lem3  11379  pfxccat3  11381  pfxccat3a  11385  swrdccat3blem  11386  redivap  11514  imdivap  11521  cvg1nlemres  11625  sqrt0  11644  summodclem3  12021  fsump1i  12074  prodf1  12183  cos1bnd  12400  odd2np1  12514  opoe  12536  omoe  12537  opeo  12538  omeo  12539  dfgcd2  12665  gcdmultiplez  12672  dvdssq  12682  algfx  12704  odzval  12894  mul4sq  13047  setsfun0  13198  rmodislmod  14447  isridl  14600  neipsm  14965  txbas  15069  elcncf1di  15390  plyco  15570  reeff1o  15584  sincosq1lem  15636  sincosq2sgn  15638  sincosq4sgn  15640  lgsne0  15857  2lgslem1  15910  mul2sq  15935  lpvtx  16020  umgrislfupgrenlem  16071  umgrislfupgrdom  16072  uspgr2wlkeq  16306  wlklenvclwlk  16314  bdbm1.3ii  16607