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  1311  19.30dc  1638  nf4r  1682  cbvexv1  1763  cbvexh  1766  equveli  1770  sbequilem  1849  sb5rf  1863  nfsbxy  1958  nfsbxyt  1959  sbcomxyyz  1988  dvelimALT  2026  dvelimfv  2027  dvelimor  2034  mo2n  2070  mo23  2083  2exeu  2134  bm1.1  2178  necon1idc  2417  sbhypf  2809  vtocl2  2815  vtocl3  2816  reu6  2949  rmo2ilem  3075  uneqin  3410  abn0r  3471  inelcm  3507  vdif0im  3512  difrab0eqim  3513  r19.3rm  3535  r19.9rmv  3538  difprsn1  3757  intminss  3895  disjnim  4020  bm1.3ii  4150  intexabim  4181  copsex2g  4275  opelopabt  4292  eusv2nf  4487  reusv3i  4490  onintrab2im  4550  ordtri2orexmid  4555  setindel  4570  onsucuni2  4596  ordtri2or2exmid  4603  zfregfr  4606  tfi  4614  mosubopt  4724  eqrelrel  4760  xpiindim  4799  opeliunxp2  4802  opelrn  4896  issref  5048  xpmlem  5086  rnxpid  5100  ssxpbm  5101  relcoi2  5196  unixpm  5201  cnviinm  5207  iotanul  5230  iotaexab  5233  funimaexglem  5337  fvelrnb  5604  fvmptssdm  5642  fnfvrnss  5718  fressnfv  5745  fconstfvm  5776  f1mpt  5814  ovprc  5953  fo1stresm  6214  fo2ndresm  6215  spc2ed  6286  opeliunxp2f  6291  reldmtpos  6306  tfrlem5  6367  tfrlem9  6372  tfri2  6419  frecfcllem  6457  frecsuclem  6459  fvmptmap  6739  ixpiinm  6778  ixp0  6785  mptelixpg  6788  ener  6833  domtr  6839  unen  6870  xpf1o  6900  mapen  6902  ss1o0el1o  6969  cardval3ex  7245  distrnqg  7447  nqnq0pi  7498  nqnq0a  7514  nqnq0m  7515  distrnq0  7519  nqprloc  7605  ltexprlemopl  7661  ltexprlemopu  7663  recexre  8597  nn1suc  9001  msqznn  9417  nn0ind  9431  fnn0ind  9433  ublbneg  9678  qreccl  9707  fzo1fzo0n0  10250  elfzom1elp1fzo  10269  fzo0end  10290  fzind2  10306  flqeqceilz  10389  nnsinds  10516  nn0sinds  10517  ser0f  10605  hashfacen  10907  iswrddm0  10938  redivap  11018  imdivap  11025  cvg1nlemres  11129  sqrt0  11148  summodclem3  11523  fsump1i  11576  prodf1  11685  cos1bnd  11902  odd2np1  12014  opoe  12036  omoe  12037  opeo  12038  omeo  12039  dfgcd2  12151  gcdmultiplez  12158  dvdssq  12168  algfx  12190  odzval  12379  mul4sq  12532  setsfun0  12654  rmodislmod  13847  isridl  14000  neipsm  14322  txbas  14426  elcncf1di  14734  reeff1o  14908  sincosq1lem  14960  sincosq2sgn  14962  sincosq4sgn  14964  lgsne0  15154  mul2sq  15203  bdbm1.3ii  15383