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  954  elrab3t  2927  difprsnss  3770  elpw2g  4199  elon2  4422  ideqg  4828  elrnmpt1s  4927  elrnmptg  4929  fun11iun  5542  eqfnfv2  5677  fmpt  5729  elunirn  5834  spc2ed  6318  tposfo2  6352  tposf12  6354  dom2lem  6862  enfii  6970  ac6sfi  6994  ltexprlemm  7712  elreal2  7942  fihasheqf1oi  10930  fprod2dlemstep  11904  bastop2  14527  2lgsoddprm  15561