| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > 3bitr4ri | Unicode version | ||
| Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 2-Sep-1995.) |
| Ref | Expression |
|---|---|
| 3bitr4i.1 |
|
| 3bitr4i.2 |
|
| 3bitr4i.3 |
|
| Ref | Expression |
|---|---|
| 3bitr4ri |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 3bitr4i.2 |
. 2
| |
| 2 | 3bitr4i.1 |
. . 3
| |
| 3 | 3bitr4i.3 |
. . 3
| |
| 4 | 2, 3 | bitr4i 187 |
. 2
|
| 5 | 1, 4 | bitr2i 185 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
| This theorem depends on definitions: df-bi 117 |
| This theorem is referenced by: dcnnOLD 850 excxor 1397 sbequ8 1869 2sb5 2010 2sb6 2011 2sb5rf 2016 2sb6rf 2017 moabs 2102 moanim 2127 2eu4 2146 2eu7 2147 sb8ab 2326 risset 2533 cbvreuvw 2743 reuind 2977 difundi 3424 indifdir 3428 unab 3439 inab 3440 rabeq0 3489 abeq0 3490 inssdif0im 3527 snprc 3697 snssOLD 3758 unipr 3863 uni0b 3874 pwtr 4262 opm 4277 onintexmid 4620 elxp2 4692 opthprc 4725 xpiundir 4733 elvvv 4737 relun 4791 inopab 4809 difopab 4810 ralxpf 4823 rexxpf 4824 dmiun 4886 rniun 5092 cnvresima 5171 imaco 5187 fnopabg 5398 dff1o2 5526 idref 5824 imaiun 5828 opabex3d 6205 opabex3 6206 onntri35 7348 elixx3g 10022 elfz2 10136 elfzuzb 10140 divalgb 12207 1nprm 12407 issubg3 13499 cnfldui 14322 alsconv 15981 |
| Copyright terms: Public domain | W3C validator |