New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  biimpa GIF version

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
StepHypRef Expression
1 biimpa.1 . . 3 (φ → (ψχ))
21biimpd 198 . 2 (φ → (ψχ))
32imp 418 1 ((φ ψ) → χ)
 Colors of variables: wff setvar class 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
 Copyright terms: Public domain W3C validator