![]() |
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 110 | . 2 ⊢ ((𝜃 ∧ 𝜓) → 𝜓) | |
2 | adantld.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
3 | 1, 2 | syl5 32 | 1 ⊢ (𝜑 → ((𝜃 ∧ 𝜓) → 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia2 107 |
This theorem is referenced by: jaoa 721 dedlema 971 dedlemb 972 prlem1 975 equveli 1770 poxp 6258 nnmordi 6542 eroprf 6655 xpdom2 6858 elni2 7344 prarloclemlo 7524 xrlttr 9827 fzen 10075 eluzgtdifelfzo 10229 ssfzo12bi 10257 climuni 11336 mulcn2 11355 serf0 11395 ntrivcvgap 11591 dfgcd2 12050 lcmgcdlem 12112 lcmdvds 12114 qnumdencl 12222 infpnlem1 12394 cnplimcim 14613 dveflem 14664 bj-charfundcALT 15039 |
Copyright terms: Public domain | W3C validator |