Theorem biimparc 293

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

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

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  biantr  893  elrab3t  2748  difprsnss  3524  elpw2g  3931  elon2  4131  ideqg  4505  elrnmpt1s  4602  elrnmptg  4604  fun11iun  5167  eqfnfv2  5287  fmpt  5340  elunirn  5426  spc2ed  5874  tposfo2  5905  tposf12  5907  dom2lem  6275  enfii  6359  ac6sfi  6379  ltexprlemm  6790  elreal2  6999