Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 3jaoi | Unicode version |
Description: Disjunction of 3 antecedents (inference). (Contributed by NM, 12-Sep-1995.) |
Ref | Expression |
---|---|
3jaoi.1 | |
3jaoi.2 | |
3jaoi.3 |
Ref | Expression |
---|---|
3jaoi |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3jaoi.1 | . . 3 | |
2 | 3jaoi.2 | . . 3 | |
3 | 3jaoi.3 | . . 3 | |
4 | 1, 2, 3 | 3pm3.2i 1160 | . 2 |
5 | 3jao 1283 | . 2 | |
6 | 4, 5 | ax-mp 5 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 w3o 962 w3a 963 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 699 |
This theorem depends on definitions: df-bi 116 df-3or 964 df-3an 965 |
This theorem is referenced by: 3jaoian 1287 3ianorr 1291 acexmidlem1 5821 nndceq 6447 nndcel 6448 znegcl 9199 xrltnr 9687 nltpnft 9719 ngtmnft 9722 xrrebnd 9724 xnegcl 9737 xnegneg 9738 xltnegi 9740 xrpnfdc 9747 xrmnfdc 9748 xnegid 9764 xaddid1 9767 xposdif 9787 prm23lt5 12142 |
Copyright terms: Public domain | W3C validator |