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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  biantr  965  elrab3t  2981  difprsnss  3853  elpw2g  4294  elon2  4523  ideqg  4933  elrnmpt1s  5034  elrnmptg  5036  fun11iun  5663  eqfnfv2  5810  fmpt  5861  elunirn  5975  spc2ed  6473  tposfo2  6543  tposf12  6545  dom2lem  7064  enfii  7182  ac6sfi  7208  ltexprlemm  7973  elreal2  8203  fihasheqf1oi  11247  fprod2dlemstep  12413  bastop2  15327  2lgsoddprm  16454