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  2928  difprsnss  3771  elpw2g  4200  elon2  4423  ideqg  4829  elrnmpt1s  4928  elrnmptg  4930  fun11iun  5543  eqfnfv2  5678  fmpt  5730  elunirn  5835  spc2ed  6319  tposfo2  6353  tposf12  6355  dom2lem  6863  enfii  6971  ac6sfi  6995  ltexprlemm  7713  elreal2  7943  fihasheqf1oi  10932  fprod2dlemstep  11933  bastop2  14556  2lgsoddprm  15590