![]() |
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-1 5 ax-2 6 ax-mp 7 ax-ia2 106 |
This theorem is referenced by: jaoa 676 dedlema 916 dedlemb 917 prlem1 920 equveli 1690 poxp 6011 nnmordi 6289 eroprf 6399 xpdom2 6601 elni2 6927 prarloclemlo 7107 xrlttr 9319 fzen 9511 eluzgtdifelfzo 9662 ssfzo12bi 9690 climuni 10735 mulcn2 10755 serf0 10795 dfgcd2 11335 lcmgcdlem 11391 lcmdvds 11393 qnumdencl 11497 |
Copyright terms: Public domain | W3C validator |