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  954  elrab3t  2919  difprsnss  3761  elpw2g  4190  elon2  4412  ideqg  4818  elrnmpt1s  4917  elrnmptg  4919  fun11iun  5528  eqfnfv2  5663  fmpt  5715  elunirn  5816  spc2ed  6300  tposfo2  6334  tposf12  6336  dom2lem  6840  enfii  6944  ac6sfi  6968  ltexprlemm  7684  elreal2  7914  fihasheqf1oi  10896  fprod2dlemstep  11804  bastop2  14404  2lgsoddprm  15438