![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > annim | Structured version Visualization version Unicode version |
Description: Express conjunction in terms of implication. (Contributed by NM, 2-Aug-1994.) |
Ref | Expression |
---|---|
annim |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | iman 430 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | con2bii 338 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() |
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 190 df-an 377 |
This theorem is referenced by: pm4.61 432 pm4.52 498 xordi 909 dfifp6 1434 exanali 1725 sbn 2221 r19.35 2905 difin0ss 3801 ordsssuc2 5490 tfindsg 6675 findsg 6708 isf34lem4 8794 hashfun 12604 isprm5 14662 mdetunilem8 19655 4cycl2vnunb 25757 strlem6 27921 hstrlem6 27929 axacprim 30340 ceqsralv2 30364 dfrdg4 30724 andnand1 31065 relowlpssretop 31769 poimirlem1 31943 poimir 31975 2exanali 36738 aifftbifffaibif 38600 |
Copyright terms: Public domain | W3C validator |