Theorem biimparc 297

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 159	. 2 |- ( ch -> ( ph -> ps ) )
3	2	imp 123	1 |- ( ( ch /\ ph ) -> ps )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  biantr  937  elrab3t  2867  difprsnss  3694  elpw2g  4117  elon2  4336  ideqg  4737  elrnmpt1s  4836  elrnmptg  4838  fun11iun  5435  eqfnfv2  5566  fmpt  5617  elunirn  5716  spc2ed  6180  tposfo2  6214  tposf12  6216  dom2lem  6717  enfii  6819  ac6sfi  6843  ltexprlemm  7520  elreal2  7750  fihasheqf1oi  10662  fprod2dlemstep  11519  bastop2  12495