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 535 | . . 3 | |
2 | 1 | anbi2i 452 | . 2 |
3 | anass 398 | . 2 | |
4 | anass 398 | . 2 | |
5 | 2, 3, 4 | 3bitr4i 211 | 1 |
Colors of variables: wff set class |
Syntax hints: wa 103 wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: an42 561 an4s 562 anandi 564 anandir 565 rnlem 945 an6 1284 2eu4 2070 reean 2576 reu2 2845 rmo4 2850 rmo3f 2854 rmo3 2972 inxp 4643 xp11m 4947 fununi 5161 fun 5265 resoprab2 5836 xporderlem 6096 poxp 6097 th3qlem1 6499 enq0enq 7207 enq0tr 7210 genpdisj 7299 cju 8687 elfzo2 9895 iooinsup 11014 summodc 11120 txbasval 12363 txcnp 12367 txlm 12375 |
Copyright terms: Public domain | W3C validator |