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  960  elrab3t  2961  difprsnss  3811  elpw2g  4246  elon2  4473  ideqg  4881  elrnmpt1s  4982  elrnmptg  4984  fun11iun  5604  eqfnfv2  5745  fmpt  5797  elunirn  5906  spc2ed  6397  tposfo2  6432  tposf12  6434  dom2lem  6944  enfii  7060  ac6sfi  7086  ltexprlemm  7819  elreal2  8049  fihasheqf1oi  11048  fprod2dlemstep  12182  bastop2  14807  2lgsoddprm  15841