NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  biimpa Unicode 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