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  936  elrab3t  2839  difprsnss  3658  elpw2g  4081  elon2  4298  ideqg  4690  elrnmpt1s  4789  elrnmptg  4791  fun11iun  5388  eqfnfv2  5519  fmpt  5570  elunirn  5667  spc2ed  6130  tposfo2  6164  tposf12  6166  dom2lem  6666  enfii  6768  ac6sfi  6792  ltexprlemm  7408  elreal2  7638  fihasheqf1oi  10534  bastop2  12253