![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > adantllr | GIF version |
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.) |
Ref | Expression |
---|---|
adantl2.1 | ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
adantllr | ⊢ ((((𝜑 ∧ 𝜏) ∧ 𝜓) ∧ 𝜒) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl 109 | . 2 ⊢ ((𝜑 ∧ 𝜏) → 𝜑) | |
2 | adantl2.1 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) | |
3 | 1, 2 | sylanl1 402 | 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-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem is referenced by: ad4ant13 513 ad4ant134 1217 r19.29an 2619 diffifi 6893 fimax2gtrilemstep 6899 cnegexlem3 8132 cnegex 8133 lemul12b 8816 climshftlemg 11305 prodeq2 11560 fprodmodd 11644 lcmdvds 12073 pw2dvdslemn 12159 dfgrp3mlem 12962 tgcl 13495 metss 13925 ivthinclemlr 14046 ivthinclemur 14048 |
Copyright terms: Public domain | W3C validator |