Theorem sylbir 134

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 132	. 2 |- ( ph -> ps )
3		sylbir.2	. 2 |- ( ps -> ch )
4	2, 3	syl 14	1 |- ( ph -> ch )

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3imtr3i  199  3ori  1282  19.30dc  1607  nf4r  1651  cbvexv1  1732  cbvexh  1735  equveli  1739  sbequilem  1818  sb5rf  1832  nfsbxy  1922  nfsbxyt  1923  sbcomxyyz  1952  dvelimALT  1990  dvelimfv  1991  dvelimor  1998  mo2n  2034  mo23  2047  2exeu  2098  bm1.1  2142  necon1idc  2380  sbhypf  2761  vtocl2  2767  vtocl3  2768  reu6  2901  rmo2ilem  3026  uneqin  3358  abn0r  3418  inelcm  3454  vdif0im  3459  difrab0eqim  3460  r19.3rm  3482  r19.9rmv  3485  difprsn1  3696  intminss  3833  disjnim  3957  bm1.3ii  4086  intexabim  4114  copsex2g  4207  opelopabt  4223  eusv2nf  4417  reusv3i  4420  onintrab2im  4478  ordtri2orexmid  4483  setindel  4498  onsucuni2  4524  ordtri2or2exmid  4531  zfregfr  4534  tfi  4542  mosubopt  4652  eqrelrel  4688  xpiindim  4724  opeliunxp2  4727  opelrn  4821  issref  4969  xpmlem  5007  rnxpid  5021  ssxpbm  5022  relcoi2  5117  unixpm  5122  cnviinm  5128  iotanul  5151  funimaexglem  5254  fvelrnb  5517  fvmptssdm  5553  fnfvrnss  5628  fressnfv  5655  fconstfvm  5686  f1mpt  5722  ovprc  5857  fo1stresm  6110  fo2ndresm  6111  spc2ed  6181  opeliunxp2f  6186  reldmtpos  6201  tfrlem5  6262  tfrlem9  6267  tfri2  6314  frecfcllem  6352  frecsuclem  6354  fvmptmap  6631  ixpiinm  6670  ixp0  6677  mptelixpg  6680  ener  6725  domtr  6731  unen  6762  xpf1o  6790  mapen  6792  ss1o0el1o  6858  cardval3ex  7121  distrnqg  7308  nqnq0pi  7359  nqnq0a  7375  nqnq0m  7376  distrnq0  7380  nqprloc  7466  ltexprlemopl  7522  ltexprlemopu  7524  recexre  8454  nn1suc  8853  msqznn  9265  nn0ind  9279  fnn0ind  9281  ublbneg  9523  qreccl  9552  fzo1fzo0n0  10086  elfzom1elp1fzo  10105  fzo0end  10126  fzind2  10142  flqeqceilz  10221  nnsinds  10346  nn0sinds  10347  ser0f  10418  hashfacen  10711  redivap  10778  imdivap  10785  cvg1nlemres  10889  sqrt0  10908  summodclem3  11281  fsump1i  11334  prodf1  11443  cos1bnd  11660  odd2np1  11768  opoe  11790  omoe  11791  opeo  11792  omeo  11793  dfgcd2  11902  gcdmultiplez  11909  dvdssq  11919  algfx  11933  odzval  12120  setsfun0  12268  neipsm  12596  txbas  12700  elcncf1di  13008  reeff1o  13136  sincosq1lem  13188  sincosq2sgn  13190  sincosq4sgn  13192  bdbm1.3ii  13508