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  2826  pssne  3365  pssn2lp  3370  ssnpss  3372  eldifn  3389  rabsnt  3797  eldifsni  3840  unimax  3925  ssintub  3944  dfnnc2  4395  nnsucelr  4428  ssfin  4470  vfinspsslem1  4550  opeliunxp  4820  opeldm  4910  dmsnopss  5067  fndm  5182  frn  5228  f1ss  5262  forn  5272  f1f1orn  5297  f1orescnv  5301  f1imacnv  5302  fun11iun  5305  tz6.12-2  5346  foelrn  5425  f1fveq  5473  isorel  5489  isoini2  5498  2ndfo  5506  fovcl  5588  weds  5938  ertr  5954  ertrd  5955  en0  6042  enpw1  6062  ncdisjun  6136  nchoicelem8  6296  nchoicelem15  6303  frecxp  6314  dmfrec  6316  fnfreclem2  6318