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  898  elrab3t  2770  difprsnss  3573  elpw2g  3990  elon2  4201  ideqg  4583  elrnmpt1s  4681  elrnmptg  4683  fun11iun  5268  eqfnfv2  5392  fmpt  5443  elunirn  5537  spc2ed  5990  tposfo2  6024  tposf12  6026  dom2lem  6479  enfii  6580  ac6sfi  6604  ltexprlemm  7149  elreal2  7358  fihasheqf1oi  10184