![]() |
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 6236 nnmordi 6520 eroprf 6631 xpdom2 6834 elni2 7316 prarloclemlo 7496 xrlttr 9798 fzen 10046 eluzgtdifelfzo 10200 ssfzo12bi 10228 climuni 11304 mulcn2 11323 serf0 11363 ntrivcvgap 11559 dfgcd2 12018 lcmgcdlem 12080 lcmdvds 12082 qnumdencl 12190 infpnlem1 12360 cnplimcim 14276 dveflem 14327 bj-charfundcALT 14701 |
Copyright terms: Public domain | W3C validator |