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  1313  19.30dc  1650  nf4r  1694  cbvexv1  1775  cbvexh  1778  equveli  1782  sbequilem  1861  sb5rf  1875  nfsbxy  1970  nfsbxyt  1971  sbcomxyyz  2000  dvelimALT  2038  dvelimfv  2039  dvelimor  2046  mo2n  2082  mo23  2095  2exeu  2146  bm1.1  2190  necon1idc  2429  sbhypf  2822  vtocl2  2828  vtocl3  2829  reu6  2962  rmo2ilem  3088  uneqin  3424  abn0r  3485  inelcm  3521  vdif0im  3526  difrab0eqim  3527  r19.3rm  3549  r19.9rmv  3552  difprsn1  3772  intminss  3910  disjnim  4035  bm1.3ii  4165  intexabim  4196  copsex2g  4290  opelopabt  4308  eusv2nf  4503  reusv3i  4506  onintrab2im  4566  ordtri2orexmid  4571  setindel  4586  onsucuni2  4612  ordtri2or2exmid  4619  zfregfr  4622  tfi  4630  mosubopt  4740  eqrelrel  4776  xpiindim  4815  opeliunxp2  4818  opelrn  4912  issref  5065  xpmlem  5103  rnxpid  5117  ssxpbm  5118  relcoi2  5213  unixpm  5218  cnviinm  5224  iotanul  5247  iotaexab  5250  funimaexglem  5357  fvelrnb  5626  fvmptssdm  5664  fnfvrnss  5740  fressnfv  5771  fconstfvm  5802  f1mpt  5840  ovprc  5980  fvmpopr2d  6082  fo1stresm  6247  fo2ndresm  6248  spc2ed  6319  opeliunxp2f  6324  reldmtpos  6339  tfrlem5  6400  tfrlem9  6405  tfri2  6452  frecfcllem  6490  frecsuclem  6492  fvmptmap  6772  ixpiinm  6811  ixp0  6818  mptelixpg  6821  ener  6871  domtr  6877  unen  6908  xpf1o  6941  mapen  6943  ss1o0el1o  7010  cardval3ex  7292  distrnqg  7500  nqnq0pi  7551  nqnq0a  7567  nqnq0m  7568  distrnq0  7572  nqprloc  7658  ltexprlemopl  7714  ltexprlemopu  7716  recexre  8651  nn1suc  9055  msqznn  9473  nn0ind  9487  fnn0ind  9489  ublbneg  9734  qreccl  9763  fzo1fzo0n0  10307  elfzom1elp1fzo  10331  fzo0end  10352  fzind2  10368  flqeqceilz  10463  nnsinds  10590  nn0sinds  10591  ser0f  10679  hashfacen  10981  iswrddm0  11018  swrdlsw  11122  redivap  11185  imdivap  11192  cvg1nlemres  11296  sqrt0  11315  summodclem3  11691  fsump1i  11744  prodf1  11853  cos1bnd  12070  odd2np1  12184  opoe  12206  omoe  12207  opeo  12208  omeo  12209  dfgcd2  12335  gcdmultiplez  12342  dvdssq  12352  algfx  12374  odzval  12564  mul4sq  12717  setsfun0  12868  rmodislmod  14113  isridl  14266  neipsm  14626  txbas  14730  elcncf1di  15051  plyco  15231  reeff1o  15245  sincosq1lem  15297  sincosq2sgn  15299  sincosq4sgn  15301  lgsne0  15515  2lgslem1  15568  mul2sq  15593  bdbm1.3ii  15831