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 1170 | . 2 |
5 | 3jao 1296 | . 2 | |
6 | 4, 5 | ax-mp 5 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 w3o 972 w3a 973 |
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 704 |
This theorem depends on definitions: df-bi 116 df-3or 974 df-3an 975 |
This theorem is referenced by: 3jaoian 1300 3ianorr 1304 acexmidlem1 5849 nndceq 6478 nndcel 6479 znegcl 9243 xrltnr 9736 nltpnft 9771 ngtmnft 9774 xrrebnd 9776 xnegcl 9789 xnegneg 9790 xltnegi 9792 xrpnfdc 9799 xrmnfdc 9800 xnegid 9816 xaddid1 9819 xposdif 9839 prm23lt5 12217 zabsle1 13694 |
Copyright terms: Public domain | W3C validator |