Theorem simprbi 450

Description: Deduction eliminating a conjunct. (Contributed by NM, 27-May-1998.)

Hypothesis

Ref	Expression
simprbi.1	|- (ph <-> (ps /\ ch))

Assertion

Ref	Expression
simprbi	|- (ph -> ch)

Proof of Theorem simprbi

Step	Hyp	Ref	Expression
1		simprbi.1	. . 3 |- (ph <-> (ps /\ ch))
2	1	biimpi 186	. 2 |- (ph -> (ps /\ ch))
3	2	simprd 449	1 |- (ph -> ch)

Syntax hints:   -> wi 4   <-> wb 176   /\ wa 358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177  df-an 360

This theorem is referenced by:  sb1  1651  eumo  2244  2eu1  2284  reurmo  2827  pssne  3366  pssn2lp  3371  ssnpss  3373  eldifn  3390  rabsnt  3798  eldifsni  3841  unimax  3926  ssintub  3945  dfnnc2  4396  nnsucelr  4429  ssfin  4471  vfinspsslem1  4551  opeliunxp  4821  opeldm  4911  dmsnopss  5068  fndm  5183  frn  5229  f1ss  5263  forn  5273  f1f1orn  5298  f1orescnv  5302  f1imacnv  5303  fun11iun  5306  tz6.12-2  5347  foelrn  5426  f1fveq  5474  isorel  5490  isoini2  5499  2ndfo  5507  fovcl  5589  weds  5939  ertr  5955  ertrd  5956  en0  6043  enpw1  6063  ncdisjun  6137  nchoicelem8  6297  nchoicelem15  6304  frecxp  6315  dmfrec  6317  fnfreclem2  6319