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  6542  tposf12  6544  dom2lem  7062  enfii  7180  ac6sfi  7206  ltexprlemm  7973  elreal2  8203  fihasheqf1oi  11248  fprod2dlemstep  12414  bastop2  15310  2lgsoddprm  16437