![]() |
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 110 |
. 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 107 |
This theorem is referenced by: jaoa 720 dedlema 969 dedlemb 970 prlem1 973 equveli 1759 poxp 6226 nnmordi 6510 eroprf 6621 xpdom2 6824 elni2 7291 prarloclemlo 7471 xrlttr 9769 fzen 10016 eluzgtdifelfzo 10170 ssfzo12bi 10198 climuni 11272 mulcn2 11291 serf0 11331 ntrivcvgap 11527 dfgcd2 11985 lcmgcdlem 12047 lcmdvds 12049 qnumdencl 12157 infpnlem1 12327 cnplimcim 13769 dveflem 13820 bj-charfundcALT 14183 |
Copyright terms: Public domain | W3C validator |