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 )

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  biantr  961  elrab3t  2972  difprsnss  3832  elpw2g  4268  elon2  4497  ideqg  4906  elrnmpt1s  5007  elrnmptg  5009  fun11iun  5635  eqfnfv2  5776  fmpt  5827  elunirn  5939  spc2ed  6429  tposfo2  6498  tposf12  6500  dom2lem  7011  enfii  7129  ac6sfi  7155  ltexprlemm  7915  elreal2  8145  fihasheqf1oi  11150  fprod2dlemstep  12308  bastop2  14949  2lgsoddprm  15986