Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > adantld | GIF 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 694 dedlema 938 dedlemb 939 prlem1 942 equveli 1717 poxp 6097 nnmordi 6380 eroprf 6490 xpdom2 6693 elni2 7090 prarloclemlo 7270 xrlttr 9549 fzen 9791 eluzgtdifelfzo 9942 ssfzo12bi 9970 climuni 11030 mulcn2 11049 serf0 11089 dfgcd2 11629 lcmgcdlem 11685 lcmdvds 11687 qnumdencl 11792 cnplimcim 12732 dveflem 12782 |
Copyright terms: Public domain | W3C validator |