![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3anim123i | Unicode version |
Description: Join antecedents and consequents with conjunction. (Contributed by NM, 8-Apr-1994.) |
Ref | Expression |
---|---|
3anim123i.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
3anim123i.2 |
![]() ![]() ![]() ![]() ![]() ![]() |
3anim123i.3 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
3anim123i |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3anim123i.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | 3ad2ant1 960 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 3anim123i.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 3 | 3ad2ant2 961 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 3anim123i.3 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
6 | 5 | 3ad2ant3 962 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 2, 4, 6 | 3jca 1119 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 df-3an 922 |
This theorem is referenced by: 3anim1i 1125 3anim2i 1126 3anim3i 1127 syl3an 1212 syl3anl 1221 spc3egv 2690 spc3gv 2691 eloprabga 5622 le2tri3i 7286 fzmmmeqm 9152 elfz1b 9183 elfz0fzfz0 9214 elfzmlbp 9220 elfzo1 9276 flltdivnn0lt 9386 modmulconst 10372 nndvdslegcd 10501 |
Copyright terms: Public domain | W3C validator |