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  2843  difprsnss  3666  elpw2g  4089  elon2  4306  ideqg  4698  elrnmpt1s  4797  elrnmptg  4799  fun11iun  5396  eqfnfv2  5527  fmpt  5578  elunirn  5675  spc2ed  6138  tposfo2  6172  tposf12  6174  dom2lem  6674  enfii  6776  ac6sfi  6800  ltexprlemm  7432  elreal2  7662  fihasheqf1oi  10566  bastop2  12292