Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > adantld | Unicode version |
Description: Deduction adding a conjunct to the left of an antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 20-Dec-2012.) |
Ref | Expression |
---|---|
adantld.1 |
Ref | Expression |
---|---|
adantld |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpr 109 | . 2 | |
2 | adantld.1 | . 2 | |
3 | 1, 2 | syl5 32 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia2 106 |
This theorem is referenced by: jaoa 709 dedlema 953 dedlemb 954 prlem1 957 equveli 1732 poxp 6122 nnmordi 6405 eroprf 6515 xpdom2 6718 elni2 7115 prarloclemlo 7295 xrlttr 9574 fzen 9816 eluzgtdifelfzo 9967 ssfzo12bi 9995 climuni 11055 mulcn2 11074 serf0 11114 ntrivcvgap 11310 dfgcd2 11691 lcmgcdlem 11747 lcmdvds 11749 qnumdencl 11854 cnplimcim 12794 dveflem 12844 |
Copyright terms: Public domain | W3C validator |