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  955  elrab3t  2935  difprsnss  3782  elpw2g  4216  elon2  4441  ideqg  4847  elrnmpt1s  4947  elrnmptg  4949  fun11iun  5565  eqfnfv2  5701  fmpt  5753  elunirn  5858  spc2ed  6342  tposfo2  6376  tposf12  6378  dom2lem  6886  enfii  6997  ac6sfi  7021  ltexprlemm  7748  elreal2  7978  fihasheqf1oi  10969  fprod2dlemstep  12048  bastop2  14671  2lgsoddprm  15705