Theorem biimparc 297

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

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  biantr  947  elrab3t  2885  difprsnss  3718  elpw2g  4142  elon2  4361  ideqg  4762  elrnmpt1s  4861  elrnmptg  4863  fun11iun  5463  eqfnfv2  5594  fmpt  5646  elunirn  5745  spc2ed  6212  tposfo2  6246  tposf12  6248  dom2lem  6750  enfii  6852  ac6sfi  6876  ltexprlemm  7562  elreal2  7792  fihasheqf1oi  10722  fprod2dlemstep  11585  bastop2  12878