Theorem biimparc 299

Description: Inference from a logical equivalence. (Contributed by NM, 3-May-1994.)

Hypothesis

Ref	Expression
biimpa.1	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
biimparc	|- ( ( ch /\ ph ) -> ps )

Proof of Theorem biimparc

Step	Hyp	Ref	Expression
1		biimpa.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2	1	biimprcd 160	. 2 |- ( ch -> ( ph -> ps ) )
3	2	imp 124	1 |- ( ( ch /\ ph ) -> ps )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  biantr  965  elrab3t  2981  difprsnss  3853  elpw2g  4292  elon2  4521  ideqg  4931  elrnmpt1s  5032  elrnmptg  5034  fun11iun  5660  eqfnfv2  5807  fmpt  5858  elunirn  5972  spc2ed  6469  tposfo2  6538  tposf12  6540  dom2lem  7058  enfii  7176  ac6sfi  7202  ltexprlemm  7967  elreal2  8197  fihasheqf1oi  11226  fprod2dlemstep  12389  bastop2  15185  2lgsoddprm  16232