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  1337  19.30dc  1676  nf4r  1719  cbvexv1  1801  cbvexh  1804  equveli  1808  sbequilem  1887  sb5rf  1901  nfsbxy  1998  nfsbxyt  1999  sbcomxyyz  2028  dvelimALT  2066  dvelimfv  2067  dvelimor  2074  mo2n  2110  mo23  2124  2exeu  2175  bm1.1  2219  necon1idc  2467  sbhypf  2866  vtocl2  2872  vtocl3  2873  reu6  3008  rmo2ilem  3135  rabssrabd  3327  uneqin  3474  abn0r  3535  inelcm  3571  vdif0im  3576  difrab0eqim  3577  r19.3rm  3600  r19.9rmv  3603  difprsn1  3835  intminss  3976  disjnim  4101  bm1.3ii  4233  intexabim  4266  copsex2g  4364  opelopabt  4382  eusv2nf  4579  reusv3i  4582  onintrab2im  4642  ordtri2orexmid  4647  setindel  4662  onsucuni2  4688  ordtri2or2exmid  4695  zfregfr  4698  tfi  4706  mosubopt  4817  eqrelrel  4853  xpiindim  4894  opeliunxp2  4897  opelrn  4993  issref  5147  xpmlem  5185  rnxpid  5199  ssxpbm  5200  relcoi2  5295  unixpm  5300  cnviinm  5306  iotanul  5330  iotaexab  5333  funimaexglem  5441  fvelrnb  5726  fvmptssdm  5764  fnfvrnss  5839  fressnfv  5873  fconstfvm  5904  f1mpt  5946  ovprc  6088  fvmpopr2d  6192  fo1stresm  6357  fo2ndresm  6358  spc2ed  6431  opeliunxp2f  6471  reldmtpos  6486  tfrlem5  6547  tfrlem9  6552  tfri2  6599  frecfcllem  6637  frecsuclem  6639  fvmptmap  6921  ixpiinm  6961  ixp0  6968  mptelixpg  6971  ener  7021  domtr  7027  unen  7060  xpf1o  7099  mapen  7101  ss1o0el1o  7175  cardval3ex  7483  pr2cv2  7495  distrnqg  7704  nqnq0pi  7755  nqnq0a  7771  nqnq0m  7772  distrnq0  7776  nqprloc  7862  ltexprlemopl  7918  ltexprlemopu  7920  recexre  8854  nn1suc  9258  msqznn  9681  nn0ind  9695  fnn0ind  9697  ublbneg  9948  qreccl  9977  fzo1fzo0n0  10526  elfzom1elp1fzo  10551  fzo0end  10572  fzind2  10589  flqeqceilz  10684  nnsinds  10811  nn0sinds  10812  ser0f  10900  hashfacen  11212  iswrddm0  11252  swrdlsw  11365  pfxn0  11384  swrdswrdlem  11400  pfxccatin12lem3  11428  pfxccat3  11430  pfxccat3a  11434  swrdccat3blem  11435  redivap  11563  imdivap  11570  cvg1nlemres  11674  sqrt0  11693  summodclem3  12070  fsump1i  12123  prodf1  12232  cos1bnd  12449  odd2np1  12563  opoe  12585  omoe  12586  opeo  12587  omeo  12588  dfgcd2  12714  gcdmultiplez  12721  dvdssq  12731  algfx  12753  odzval  12943  mul4sq  13096  setsfun0  13265  rmodislmod  14516  isridl  14669  neipsm  15036  txbas  15140  elcncf1di  15461  plyco  15641  reeff1o  15655  sincosq1lem  15707  sincosq2sgn  15709  sincosq4sgn  15711  lgsne0  15928  2lgslem1  15981  mul2sq  16006  lpvtx  16091  umgrislfupgrenlem  16142  umgrislfupgrdom  16143  uspgr2wlkeq  16377  wlklenvclwlk  16385  bdbm1.3ii  16678