![]() |
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 6896 fimax2gtrilemstep 6902 cnegexlem3 8136 cnegex 8137 lemul12b 8820 climshftlemg 11312 prodeq2 11567 fprodmodd 11651 lcmdvds 12081 pw2dvdslemn 12167 dfgrp3mlem 12973 tgcl 13603 metss 14033 ivthinclemlr 14154 ivthinclemur 14156 |
Copyright terms: Public domain | W3C validator |