![]() |
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: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia2 106 |
This theorem is referenced by: jaoa 710 dedlema 954 dedlemb 955 prlem1 958 equveli 1733 poxp 6137 nnmordi 6420 eroprf 6530 xpdom2 6733 elni2 7146 prarloclemlo 7326 xrlttr 9611 fzen 9854 eluzgtdifelfzo 10005 ssfzo12bi 10033 climuni 11094 mulcn2 11113 serf0 11153 ntrivcvgap 11349 dfgcd2 11738 lcmgcdlem 11794 lcmdvds 11796 qnumdencl 11901 cnplimcim 12844 dveflem 12895 |
Copyright terms: Public domain | W3C validator |