Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > an32 | Unicode version |
Description: A rearrangement of conjuncts. (Contributed by NM, 12-Mar-1995.) (Proof shortened by Wolf Lammen, 25-Dec-2012.) |
Ref | Expression |
---|---|
an32 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | anass 398 | . 2 | |
2 | an12 535 | . 2 | |
3 | ancom 264 | . 2 | |
4 | 1, 2, 3 | 3bitri 205 | 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: an32s 542 3anan32 958 indifdir 3302 inrab2 3319 reupick 3330 unidif0 4061 resco 5013 f11o 5368 respreima 5516 dff1o6 5645 dfoprab2 5786 xpassen 6692 enq0enq 7207 elioomnf 9719 modfsummod 11195 tx1cn 12365 isms2 12550 elcncf1di 12662 |
Copyright terms: Public domain | W3C validator |