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

Theorem annim 414
Description: Express conjunction in terms of implication. (Contributed by NM, 2-Aug-1994.)
Assertion
Ref Expression
annim

Proof of Theorem annim
StepHypRef Expression
1 iman 413 . 2
21con2bii 322 1
Colors of variables: wff setvar class
Syntax hints:   wn 3   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:  pm4.61  415  pm4.52  477  xordi  865  exanali  1585  19.35  1600  rexanali  2660  r19.35  2758  difin0ss  3616  dfpw2  4327  nnsucelrlem1  4424  evenodddisjlem1  4515  nnadjoinlem1  4519  sfintfinlem1  4531  tfinnnlem1  4533  nchoicelem10  6298  nchoicelem11  6299
  Copyright terms: Public domain W3C validator