Theorem biimpa 470

Description: Inference from a logical equivalence. (Contributed by NM, 3-May-1994.)

Hypothesis

Ref	Expression
biimpa.1	|- (ph -> (ps <-> ch))

Assertion

Ref	Expression
biimpa	|- ((ph /\ ps) -> ch)

Proof of Theorem biimpa

Step	Hyp	Ref	Expression
1		biimpa.1	. . 3 |- (ph -> (ps <-> ch))
2	1	biimpd 198	. 2 |- (ph -> (ps -> ch))
3	2	imp 418	1 |- ((ph /\ ps) -> ch)

Syntax hints:   -> wi 4   <-> wb 176   /\ wa 358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177  df-an 360

This theorem is referenced by:  simprbda  606  simplbda  607  pm5.1  830  bimsc1  904  biimp3a  1281  euor  2231  euan  2261  cgsexg  2891  cgsex2g  2892  cgsex4g  2893  ceqsex  2894  sbciegft  3077  sbeqalb  3099  syl5sseq  3320  ltfintr  4460  ssfin  4471  vfinspss  4552  f1o00  5318  f1o2d  5728  lectr  6212  nclenn  6250  ncslesuc  6268  fnfrec  6321