Theorem biimpa 470

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

Hypothesis

Ref	Expression
biimpa.1	⊢ (φ → (ψ ↔ χ))

Assertion

Ref	Expression
biimpa	⊢ ((φ ∧ ψ) → χ)

Proof of Theorem biimpa

Step	Hyp	Ref	Expression
1		biimpa.1	. . 3 ⊢ (φ → (ψ ↔ χ))
2	1	biimpd 198	. 2 ⊢ (φ → (ψ → χ))
3	2	imp 418	1 ⊢ ((φ ∧ ψ) → χ)

Syntax hints:   → wi 4   ↔ wb 176   ∧ wa 358

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 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  2890  cgsex2g  2891  cgsex4g  2892  ceqsex  2893  sbciegft  3076  sbeqalb  3098  syl5sseq  3319  ltfintr  4459  ssfin  4470  vfinspss  4551  f1o00  5317  f1o2d  5727  lectr  6211  nclenn  6249  ncslesuc  6267  fnfrec  6320