![]() |
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 256 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | bitr2i 254 |
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 189 |
This theorem is referenced by: pm4.78 586 xor 902 nannan 1389 nanbiOLDOLD 1395 nic-ax 1556 2sb5 2272 2sb6 2273 2sb5rf 2280 moabs 2330 2mo2 2379 2eu7 2388 2eu8 2389 r3al 2768 r2exlem 2910 risset 2915 r19.35 2937 ralxpxfr2d 3164 reuind 3243 undif3 3704 unab 3710 inab 3711 inssdif0 3834 ssundif 3851 snss 4096 raldifsnb 4103 pwtp 4195 unipr 4211 uni0b 4223 iinuni 4365 reusv2lem4 4607 pwtr 4653 elxp2 4852 opthprc 4882 xpiundir 4890 elvvv 4894 xpsspw 4948 relun 4950 inopab 4965 difopab 4966 ralxpf 4981 dmiun 5043 inisegn0 5200 rniun 5246 cnvresima 5324 imaco 5340 mptfnf 5699 fnopabg 5701 dff1o2 5819 brprcneu 5858 idref 6146 imaiun 6150 sorpss 6576 opabex3d 6771 opabex3 6772 ovmptss 6877 fnsuppres 6942 rankc1 8341 aceq1 8548 dfac10 8567 fin41 8874 axgroth6 9253 genpass 9434 infm3 10568 prime 11016 elixx3g 11648 elfz2 11791 elfzuzb 11794 rpnnen2 14278 divalgb 14385 1nprm 14629 maxprmfct 14652 vdwmc 14928 imasleval 15447 issubm 16594 issubg3 16835 efgrelexlemb 17400 ist1-2 20363 unisngl 20542 elflim2 20979 isfcls 21024 istlm 21199 isnlm 21678 ishl2 22337 0wlk 25275 0trl 25276 erclwwlkref 25541 erclwwlknref 25553 h1de2ctlem 27208 nonbooli 27304 5oalem7 27313 ho01i 27481 rnbra 27760 cvnbtwn3 27941 chrelat2i 28018 moel 28119 uniinn0 28163 disjex 28202 maprnin 28316 ordtconlem1 28730 esum2dlem 28913 eulerpartgbij 29205 eulerpartlemr 29207 eulerpartlemn 29214 ballotlem2 29321 bnj976 29589 bnj1185 29605 bnj543 29704 bnj571 29717 bnj611 29729 bnj916 29744 bnj1000 29752 bnj1040 29781 iscvm 29982 untuni 30336 dfso3 30352 dffr5 30393 nofulllem5 30595 brtxpsd3 30663 brbigcup 30665 fixcnv 30675 ellimits 30677 elfuns 30682 brimage 30693 brcart 30699 brimg 30704 brapply 30705 brcup 30706 brcap 30707 dfrdg4 30718 dfint3 30719 ellines 30919 elicc3 30973 bj-ssb1 31246 bj-snsetex 31557 bj-snglc 31563 bj-projun 31588 bj-vjust2 31619 wl-cases2-dnf 31850 poimirlem27 31967 mblfinlem2 31978 iscrngo2 32231 prtlem70 32425 prtlem100 32429 n0el 32433 prtlem15 32447 prter2 32453 lcvnbtwn3 32594 ishlat1 32918 ishlat2 32919 hlrelat2 32968 islpln5 33100 islvol5 33144 pclclN 33456 cdleme0nex 33856 aaitgo 36028 isdomn3 36081 imaiun1 36243 relexp0eq 36293 2sbc6g 36766 2sbc5g 36767 2reu7 38612 2reu8 38613 01wlk 39704 alsconv 40582 |
Copyright terms: Public domain | W3C validator |