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  5681  fvmptssdm  5719  fnfvrnss  5795  fressnfv  5826  fconstfvm  5857  f1mpt  5895  ovprc  6037  fvmpopr2d  6141  fo1stresm  6307  fo2ndresm  6308  spc2ed  6379  opeliunxp2f  6384  reldmtpos  6399  tfrlem5  6460  tfrlem9  6465  tfri2  6512  frecfcllem  6550  frecsuclem  6552  fvmptmap  6832  ixpiinm  6871  ixp0  6878  mptelixpg  6881  ener  6931  domtr  6937  unen  6969  xpf1o  7005  mapen  7007  ss1o0el1o  7075  cardval3ex  7357  pr2cv2  7369  distrnqg  7574  nqnq0pi  7625  nqnq0a  7641  nqnq0m  7642  distrnq0  7646  nqprloc  7732  ltexprlemopl  7788  ltexprlemopu  7790  recexre  8725  nn1suc  9129  msqznn  9547  nn0ind  9561  fnn0ind  9563  ublbneg  9808  qreccl  9837  fzo1fzo0n0  10383  elfzom1elp1fzo  10408  fzo0end  10429  fzind2  10445  flqeqceilz  10540  nnsinds  10667  nn0sinds  10668  ser0f  10756  hashfacen  11058  iswrddm0  11095  swrdlsw  11201  pfxn0  11220  swrdswrdlem  11236  pfxccatin12lem3  11264  pfxccat3  11266  pfxccat3a  11270  swrdccat3blem  11271  redivap  11385  imdivap  11392  cvg1nlemres  11496  sqrt0  11515  summodclem3  11891  fsump1i  11944  prodf1  12053  cos1bnd  12270  odd2np1  12384  opoe  12406  omoe  12407  opeo  12408  omeo  12409  dfgcd2  12535  gcdmultiplez  12542  dvdssq  12552  algfx  12574  odzval  12764  mul4sq  12917  setsfun0  13068  rmodislmod  14315  isridl  14468  neipsm  14828  txbas  14932  elcncf1di  15253  plyco  15433  reeff1o  15447  sincosq1lem  15499  sincosq2sgn  15501  sincosq4sgn  15503  lgsne0  15717  2lgslem1  15770  mul2sq  15795  lpvtx  15879  umgrislfupgrenlem  15928  umgrislfupgrdom  15929  uspgr2wlkeq  16076  wlklenvclwlk  16084  bdbm1.3ii  16254