![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3anbi123d | Unicode version |
Description: Deduction joining 3 equivalences to form equivalence of conjunctions. (Contributed by NM, 22-Apr-1994.) |
Ref | Expression |
---|---|
bi3d.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
bi3d.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
bi3d.3 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
3anbi123d |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bi3d.1 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | bi3d.2 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | anbi12d 473 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | bi3d.3 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 4 | anbi12d 473 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | df-3an 980 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | df-3an 980 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
8 | 5, 6, 7 | 3bitr4g 223 |
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 df-3an 980 |
This theorem is referenced by: 3anbi12d 1313 3anbi13d 1314 3anbi23d 1315 limeq 4377 smoeq 6290 tfrlemi1 6332 tfr1onlemaccex 6348 tfrcllemaccex 6361 ereq1 6541 updjud 7080 ctssdclemr 7110 tapeq1 7250 tapeq2 7251 elinp 7472 sup3exmid 8912 iccshftr 9992 iccshftl 9994 iccdil 9996 icccntr 9998 fzaddel 10056 elfzomelpfzo 10228 seq3f1olemstep 10498 seq3f1olemp 10499 sumeq1 11358 summodclem2 11385 summodc 11386 zsumdc 11387 prodmodclem2 11580 prodmodc 11581 divalglemnn 11917 divalglemeunn 11920 divalglemeuneg 11922 dfgcd2 12009 pythagtriplem18 12275 pythagtriplem19 12276 ctiunct 12435 ssomct 12440 isstruct2im 12466 isstruct2r 12467 ptex 12707 isringd 13213 issubrg3 13368 fiinopn 13435 lmfval 13623 upxp 13703 2irrexpqap 14327 dceqnconst 14727 dcapnconst 14728 |
Copyright terms: Public domain | W3C validator |