Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > an4 | Unicode version |
Description: Rearrangement of 4 conjuncts. (Contributed by NM, 10-Jul-1994.) |
Ref | Expression |
---|---|
an4 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | an12 495 | . . 3 | |
2 | 1 | anbi2i 430 | . 2 |
3 | anass 381 | . 2 | |
4 | anass 381 | . 2 | |
5 | 2, 3, 4 | 3bitr4i 201 | 1 |
Colors of variables: wff set class |
Syntax hints: wa 97 wb 98 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: an42 521 an4s 522 anandi 524 anandir 525 rnlem 883 an6 1216 2eu4 1993 reean 2478 reu2 2729 rmo4 2734 rmo3 2849 inxp 4470 xp11m 4759 fununi 4967 fun 5063 resoprab2 5598 xporderlem 5852 poxp 5853 th3qlem1 6208 enq0enq 6529 enq0tr 6532 genpdisj 6621 cju 7913 elfzo2 9007 |
Copyright terms: Public domain | W3C validator |