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 )

Syntax hints:   -> wi 4   /\ wa 104   <-> 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:  biantr  965  elrab3t  2981  difprsnss  3848  elpw2g  4287  elon2  4516  ideqg  4926  elrnmpt1s  5027  elrnmptg  5029  fun11iun  5655  eqfnfv2  5798  fmpt  5849  elunirn  5962  spc2ed  6459  tposfo2  6528  tposf12  6530  dom2lem  7048  enfii  7166  ac6sfi  7192  ltexprlemm  7957  elreal2  8187  fihasheqf1oi  11204  fprod2dlemstep  12367  bastop2  15108  2lgsoddprm  16146