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 108 | . 2 ⊢ ((𝜑 ∧ 𝜏) → 𝜑) | |
2 | adantl2.1 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) | |
3 | 1, 2 | sylanl1 400 | 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-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem is referenced by: ad4ant13 505 ad4ant134 1199 r19.29an 2599 diffifi 6839 fimax2gtrilemstep 6845 cnegexlem3 8052 cnegex 8053 lemul12b 8732 climshftlemg 11199 prodeq2 11454 fprodmodd 11538 lcmdvds 11955 pw2dvdslemn 12039 tgcl 12464 metss 12894 ivthinclemlr 13015 ivthinclemur 13017 |
Copyright terms: Public domain | W3C validator |