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 925 | . 2 |
3 | 3anim123i.2 | . . 3 | |
4 | 3 | 3ad2ant2 926 | . 2 |
5 | 3anim123i.3 | . . 3 | |
6 | 5 | 3ad2ant3 927 | . 2 |
7 | 2, 4, 6 | 3jca 1084 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 w3a 885 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 df-3an 887 |
This theorem is referenced by: 3anim1i 1090 3anim2i 1091 3anim3i 1092 syl3an 1177 syl3anl 1186 spc3egv 2644 spc3gv 2645 eloprabga 5591 le2tri3i 7126 fzmmmeqm 8921 elfz1b 8952 elfz0fzfz0 8983 elfzmlbmOLD 8989 elfzmlbp 8990 elfzo1 9046 flltdivnn0lt 9146 |
Copyright terms: Public domain | W3C validator |