Theorem simplbi 446

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

Hypothesis

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

Assertion

Ref	Expression
simplbi	|- (ph -> ps)

Proof of Theorem simplbi

Step	Hyp	Ref	Expression
1		simplbi.1	. . 3 |- (ph <-> (ps /\ ch))
2	1	biimpi 186	. 2 |- (ph -> (ps /\ ch))
3	2	simpld 445	1 |- (ph -> ps)

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:  3simpa  952  reurex  2826  eqimss  3324  pssss  3365  eldifi  3389  inss1  3476  ssunsn2  3866  fnfun  5182  ffn  5224  f1f  5259  f1of1  5287  f1ofo  5294  nfvres  5353  ressnop0  5437  isof1o  5489  1stfo  5506  oprabid  5551  brtxp  5784  otelins2  5792  otelins3  5793  oqelins4  5795  weds  5939  ersym  5953  nchoicelem4  6293  nchoicelem8  6297  nchoicelem9  6298  nchoicelem19  6308  fnfreclem3  6320