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  954  elrab3t  2907  difprsnss  3745  elpw2g  4171  elon2  4391  ideqg  4793  elrnmpt1s  4892  elrnmptg  4894  fun11iun  5497  eqfnfv2  5630  fmpt  5682  elunirn  5783  spc2ed  6252  tposfo2  6286  tposf12  6288  dom2lem  6790  enfii  6892  ac6sfi  6916  ltexprlemm  7617  elreal2  7847  fihasheqf1oi  10785  fprod2dlemstep  11648  bastop2  13981