Theorem biimparc 283

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

Syntax hints:   -> wi 4   /\ wa 97   <-> wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  biantr  859  elrab3t  2697  difprsnss  3502  elpw2g  3910  elon2  4113  ideqg  4487  elrnmpt1s  4584  elrnmptg  4586  fun11iun  5147  eqfnfv2  5266  fmpt  5319  elunirn  5405  tposfo2  5882  tposf12  5884  dom2lem  6252  enfii  6335  ac6sfi  6352  ltexprlemm  6698  elreal2  6907