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  894  elrab3t  2749  difprsnss  3532  elpw2g  3939  elon2  4139  ideqg  4515  elrnmpt1s  4612  elrnmptg  4614  fun11iun  5178  eqfnfv2  5298  fmpt  5351  elunirn  5437  spc2ed  5885  tposfo2  5916  tposf12  5918  dom2lem  6319  enfii  6409  ac6sfi  6431  ltexprlemm  6852  elreal2  7061  sizeeqf1oi  9812