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  4166  intexabim  4197  copsex2g  4291  opelopabt  4309  eusv2nf  4504  reusv3i  4507  onintrab2im  4567  ordtri2orexmid  4572  setindel  4587  onsucuni2  4613  ordtri2or2exmid  4620  zfregfr  4623  tfi  4631  mosubopt  4741  eqrelrel  4777  xpiindim  4816  opeliunxp2  4819  opelrn  4913  issref  5066  xpmlem  5104  rnxpid  5118  ssxpbm  5119  relcoi2  5214  unixpm  5219  cnviinm  5225  iotanul  5248  iotaexab  5251  funimaexglem  5358  fvelrnb  5628  fvmptssdm  5666  fnfvrnss  5742  fressnfv  5773  fconstfvm  5804  f1mpt  5842  ovprc  5982  fvmpopr2d  6084  fo1stresm  6249  fo2ndresm  6250  spc2ed  6321  opeliunxp2f  6326  reldmtpos  6341  tfrlem5  6402  tfrlem9  6407  tfri2  6454  frecfcllem  6492  frecsuclem  6494  fvmptmap  6774  ixpiinm  6813  ixp0  6820  mptelixpg  6823  ener  6873  domtr  6879  unen  6910  xpf1o  6943  mapen  6945  ss1o0el1o  7012  cardval3ex  7294  distrnqg  7502  nqnq0pi  7553  nqnq0a  7569  nqnq0m  7570  distrnq0  7574  nqprloc  7660  ltexprlemopl  7716  ltexprlemopu  7718  recexre  8653  nn1suc  9057  msqznn  9475  nn0ind  9489  fnn0ind  9491  ublbneg  9736  qreccl  9765  fzo1fzo0n0  10309  elfzom1elp1fzo  10333  fzo0end  10354  fzind2  10370  flqeqceilz  10465  nnsinds  10592  nn0sinds  10593  ser0f  10681  hashfacen  10983  iswrddm0  11020  swrdlsw  11125  pfxn0  11142  redivap  11218  imdivap  11225  cvg1nlemres  11329  sqrt0  11348  summodclem3  11724  fsump1i  11777  prodf1  11886  cos1bnd  12103  odd2np1  12217  opoe  12239  omoe  12240  opeo  12241  omeo  12242  dfgcd2  12368  gcdmultiplez  12375  dvdssq  12385  algfx  12407  odzval  12597  mul4sq  12750  setsfun0  12901  rmodislmod  14146  isridl  14299  neipsm  14659  txbas  14763  elcncf1di  15084  plyco  15264  reeff1o  15278  sincosq1lem  15330  sincosq2sgn  15332  sincosq4sgn  15334  lgsne0  15548  2lgslem1  15601  mul2sq  15626  bdbm1.3ii  15864