| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > 3ad2antl2 | Unicode version | ||
| Description: Deduction adding conjuncts to antecedent. (Contributed by NM, 4-Aug-2007.) |
| Ref | Expression |
|---|---|
| 3ad2antl.1 |
|
| Ref | Expression |
|---|---|
| 3ad2antl2 |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 3ad2antl.1 |
. . 3
| |
| 2 | 1 | adantlr 477 |
. 2
|
| 3 | 2 | 3adantl1 1179 |
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 1006 |
| This theorem is referenced by: fcofo 5925 cocan1 5928 acexmid 6017 caovimo 6216 ordiso2 7234 mkvprop 7357 ltpopr 7815 ltsopr 7816 addcanprleml 7834 addcanprlemu 7835 aptiprlemu 7860 seq1g 10726 dvdsmodexp 12358 muldvds1 12379 lcmdvds 12653 cnpnei 14946 upgrpredgv 16000 |
| Copyright terms: Public domain | W3C validator |