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  958  elrab3t  2958  difprsnss  3805  elpw2g  4239  elon2  4466  ideqg  4872  elrnmpt1s  4973  elrnmptg  4975  fun11iun  5592  eqfnfv2  5732  fmpt  5784  elunirn  5889  spc2ed  6377  tposfo2  6411  tposf12  6413  dom2lem  6921  enfii  7032  ac6sfi  7056  ltexprlemm  7783  elreal2  8013  fihasheqf1oi  11004  fprod2dlemstep  12128  bastop2  14752  2lgsoddprm  15786