Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > an12 | Unicode version |
Description: Swap two conjuncts. Note that the first digit (1) in the label refers to the outer conjunct position, and the next digit (2) to the inner conjunct position. (Contributed by NM, 12-Mar-1995.) |
Ref | Expression |
---|---|
an12 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ancom 253 | . . 3 | |
2 | 1 | anbi1i 431 | . 2 |
3 | anass 381 | . 2 | |
4 | anass 381 | . 2 | |
5 | 2, 3, 4 | 3bitr3i 199 | 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: an32 496 an13 497 an12s 499 an4 520 ceqsrexv 2674 rmoan 2739 2reuswapdc 2743 reuind 2744 2rmorex 2745 sbccomlem 2832 elunirab 3593 rexxfrd 4195 opeliunxp 4395 elres 4646 resoprab 5597 ov6g 5638 opabex3d 5748 opabex3 5749 xpassen 6304 distrnqg 6485 distrnq0 6557 rexuz2 8524 2clim 9822 |
Copyright terms: Public domain | W3C validator |