![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3bitr4ri | Structured version Visualization version 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 260 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | bitr2i 258 |
1
![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 190 |
This theorem is referenced by: pm4.78 592 xor 908 nannan 1416 nic-ax 1564 2sb5 2292 2sb6 2293 2sb5rf 2300 moabs 2350 2mo2 2399 2eu7 2408 2eu8 2409 r3al 2784 r2exlem 2899 risset 2902 r19.35 2923 ralxpxfr2d 3152 reuind 3231 undif3 3695 unab 3701 inab 3702 inssdif0 3746 ssundif 3842 snss 4087 raldifsnb 4094 pwtp 4187 unipr 4203 uni0b 4215 iinuni 4358 reusv2lem4 4605 pwtr 4653 elxp2 4857 opthprc 4887 xpiundir 4895 elvvv 4899 xpsspw 4953 relun 4955 inopab 4970 difopab 4971 ralxpf 4986 dmiun 5049 inisegn0 5206 rniun 5252 cnvresima 5331 imaco 5347 mptfnf 5709 fnopabg 5711 dff1o2 5833 brprcneu 5872 idref 6164 imaiun 6168 sorpss 6595 opabex3d 6790 opabex3 6791 ovmptss 6896 fnsuppres 6961 rankc1 8359 aceq1 8566 dfac10 8585 fin41 8892 axgroth6 9271 genpass 9452 infm3 10590 prime 11039 elixx3g 11673 elfz2 11817 elfzuzb 11820 rpnnen2 14355 divalgb 14464 1nprm 14708 maxprmfct 14731 vdwmc 15007 imasleval 15525 issubm 16672 issubg3 16913 efgrelexlemb 17478 ist1-2 20440 unisngl 20619 elflim2 21057 isfcls 21102 istlm 21277 isnlm 21756 ishl2 22415 0wlk 25354 0trl 25355 erclwwlkref 25620 erclwwlknref 25632 h1de2ctlem 27289 nonbooli 27385 5oalem7 27394 ho01i 27562 rnbra 27841 cvnbtwn3 28022 chrelat2i 28099 moel 28198 uniinn0 28241 disjex 28279 maprnin 28391 ordtconlem1 28804 esum2dlem 28987 eulerpartgbij 29278 eulerpartlemr 29280 eulerpartlemn 29287 ballotlem2 29394 bnj976 29661 bnj1185 29677 bnj543 29776 bnj571 29789 bnj611 29801 bnj916 29816 bnj1000 29824 bnj1040 29853 iscvm 30054 untuni 30408 dfso3 30424 dffr5 30464 nofulllem5 30666 brtxpsd3 30734 brbigcup 30736 fixcnv 30746 ellimits 30748 elfuns 30753 brimage 30764 brcart 30770 brimg 30775 brapply 30776 brcup 30777 brcap 30778 dfrdg4 30789 dfint3 30790 ellines 30990 elicc3 31044 bj-ssb1 31310 bj-snsetex 31627 bj-snglc 31633 bj-projun 31658 bj-vjust2 31689 wl-cases2-dnf 31920 poimirlem27 32031 mblfinlem2 32042 iscrngo2 32295 prtlem70 32489 prtlem100 32493 n0el 32497 prtlem15 32511 prter2 32517 lcvnbtwn3 32665 ishlat1 32989 ishlat2 32990 hlrelat2 33039 islpln5 33171 islvol5 33215 pclclN 33527 cdleme0nex 33927 aaitgo 36099 isdomn3 36152 imaiun1 36314 relexp0eq 36364 2sbc6g 36836 2sbc5g 36837 2reu7 38757 2reu8 38758 01wlk 40005 alsconv 41035 |
Copyright terms: Public domain | W3C validator |