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  1334  19.30dc  1673  nf4r  1717  cbvexv1  1798  cbvexh  1801  equveli  1805  sbequilem  1884  sb5rf  1898  nfsbxy  1993  nfsbxyt  1994  sbcomxyyz  2023  dvelimALT  2061  dvelimfv  2062  dvelimor  2069  mo2n  2105  mo23  2119  2exeu  2170  bm1.1  2214  necon1idc  2453  sbhypf  2850  vtocl2  2856  vtocl3  2857  reu6  2992  rmo2ilem  3119  uneqin  3455  abn0r  3516  inelcm  3552  vdif0im  3557  difrab0eqim  3558  r19.3rm  3580  r19.9rmv  3583  difprsn1  3807  intminss  3948  disjnim  4073  bm1.3ii  4205  intexabim  4236  copsex2g  4332  opelopabt  4350  eusv2nf  4547  reusv3i  4550  onintrab2im  4610  ordtri2orexmid  4615  setindel  4630  onsucuni2  4656  ordtri2or2exmid  4663  zfregfr  4666  tfi  4674  mosubopt  4784  eqrelrel  4820  xpiindim  4859  opeliunxp2  4862  opelrn  4958  issref  5111  xpmlem  5149  rnxpid  5163  ssxpbm  5164  relcoi2  5259  unixpm  5264  cnviinm  5270  iotanul  5294  iotaexab  5297  funimaexglem  5404  fvelrnb  5683  fvmptssdm  5721  fnfvrnss  5797  fressnfv  5830  fconstfvm  5861  f1mpt  5901  ovprc  6043  fvmpopr2d  6147  fo1stresm  6313  fo2ndresm  6314  spc2ed  6385  opeliunxp2f  6390  reldmtpos  6405  tfrlem5  6466  tfrlem9  6471  tfri2  6518  frecfcllem  6556  frecsuclem  6558  fvmptmap  6840  ixpiinm  6879  ixp0  6886  mptelixpg  6889  ener  6939  domtr  6945  unen  6977  xpf1o  7013  mapen  7015  ss1o0el1o  7086  cardval3ex  7368  pr2cv2  7380  distrnqg  7585  nqnq0pi  7636  nqnq0a  7652  nqnq0m  7653  distrnq0  7657  nqprloc  7743  ltexprlemopl  7799  ltexprlemopu  7801  recexre  8736  nn1suc  9140  msqznn  9558  nn0ind  9572  fnn0ind  9574  ublbneg  9820  qreccl  9849  fzo1fzo0n0  10395  elfzom1elp1fzo  10420  fzo0end  10441  fzind2  10457  flqeqceilz  10552  nnsinds  10679  nn0sinds  10680  ser0f  10768  hashfacen  11071  iswrddm0  11108  swrdlsw  11217  pfxn0  11236  swrdswrdlem  11252  pfxccatin12lem3  11280  pfxccat3  11282  pfxccat3a  11286  swrdccat3blem  11287  redivap  11401  imdivap  11408  cvg1nlemres  11512  sqrt0  11531  summodclem3  11907  fsump1i  11960  prodf1  12069  cos1bnd  12286  odd2np1  12400  opoe  12422  omoe  12423  opeo  12424  omeo  12425  dfgcd2  12551  gcdmultiplez  12558  dvdssq  12568  algfx  12590  odzval  12780  mul4sq  12933  setsfun0  13084  rmodislmod  14331  isridl  14484  neipsm  14844  txbas  14948  elcncf1di  15269  plyco  15449  reeff1o  15463  sincosq1lem  15515  sincosq2sgn  15517  sincosq4sgn  15519  lgsne0  15733  2lgslem1  15786  mul2sq  15811  lpvtx  15895  umgrislfupgrenlem  15944  umgrislfupgrdom  15945  uspgr2wlkeq  16111  wlklenvclwlk  16119  bdbm1.3ii  16337