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  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  3852  intminss  3993  disjnim  4118  bm1.3ii  4252  intexabim  4286  copsex2g  4384  opelopabt  4402  eusv2nf  4600  reusv3i  4603  onintrab2im  4663  ordtri2orexmid  4668  setindel  4683  onsucuni2  4709  ordtri2or2exmid  4716  zfregfr  4719  tfi  4727  mosubopt  4838  eqrelrel  4874  xpiindim  4915  opeliunxp2  4918  opelrn  5014  issref  5168  xpmlem  5206  rnxpid  5220  ssxpbm  5221  relcoi2  5316  unixpm  5321  cnviinm  5327  iotanul  5351  iotaexab  5354  funimaexglem  5462  fvelrnb  5747  fvmptssdm  5787  fnfvrnss  5862  fressnfv  5896  fconstfvm  5927  f1mpt  5970  ovprc  6114  fvmpopr2d  6218  fo1stresm  6388  fo2ndresm  6389  spc2ed  6462  opeliunxp2f  6502  reldmtpos  6517  tfrlem5  6578  tfrlem9  6583  tfri2  6630  frecfcllem  6668  frecsuclem  6670  fvmptmap  6959  ixpiinm  6999  ixp0  7006  mptelixpg  7009  ener  7059  domtr  7065  unen  7098  xpf1o  7137  mapen  7139  ss1o0el1o  7213  cardval3ex  7523  pr2cv2  7535  distrnqg  7747  nqnq0pi  7798  nqnq0a  7814  nqnq0m  7815  distrnq0  7819  nqprloc  7905  ltexprlemopl  7961  ltexprlemopu  7963  recexre  8899  nn1suc  9305  msqznn  9728  nn0ind  9742  fnn0ind  9744  ublbneg  9995  qreccl  10024  fzo1fzo0n0  10576  elfzom1elp1fzo  10601  fzo0end  10622  fzind2  10639  flqeqceilz  10736  nnsinds  10863  nn0sinds  10864  ser0f  10952  hashfacen  11265  iswrddm0  11309  swrdlsw  11422  pfxn0  11441  swrdswrdlem  11457  pfxccatin12lem3  11485  pfxccat3  11487  pfxccat3a  11491  swrdccat3blem  11492  redivap  11620  imdivap  11627  cvg1nlemres  11732  sqrt0  11751  summodclem3  12128  fsump1i  12181  prodf1  12290  cos1bnd  12507  odd2np1  12621  opoe  12643  omoe  12644  opeo  12645  omeo  12646  dfgcd2  12772  gcdmultiplez  12779  dvdssq  12789  algfx  12811  odzval  13001  mul4sq  13154  ballotfilemsdom  13236  ballotfilemth  13262  setsfun0  13369  rmodislmod  14663  isridl  14816  neipsm  15181  txbas  15285  elcncf1di  15606  plyco  15786  reeff1o  15800  sincosq1lem  15852  sincosq2sgn  15854  sincosq4sgn  15856  lgsne0  16074  2lgslem1  16127  mul2sq  16152  lpvtx  16237  umgrislfupgrenlem  16288  umgrislfupgrdom  16289  uspgr2wlkeq  16523  wlklenvclwlk  16531  bdbm1.3ii  16834  als-no-surprise  17055