![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > adantlrl | Structured version Visualization version 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 |
---|---|
adantlrl | ⊢ (((𝜑 ∧ (𝜏 ∧ 𝜓)) ∧ 𝜒) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpr 476 | . 2 ⊢ ((𝜏 ∧ 𝜓) → 𝜓) | |
2 | adantl2.1 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) | |
3 | 1, 2 | sylanl2 684 | 1 ⊢ (((𝜑 ∧ (𝜏 ∧ 𝜓)) ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 197 df-an 385 |
This theorem is referenced by: omlimcl 7703 odi 7704 oelim2 7720 mapxpen 8167 unwdomg 8530 dfac12lem2 9004 infunsdom 9074 fin1a2s 9274 frlmup1 20185 fbasrn 21735 lmmbr 23102 grporcan 27500 unoplin 28907 hmoplin 28929 superpos 29341 subfacp1lem5 31292 matunitlindflem1 33535 poimirlem4 33543 itg2addnclem 33591 ftc1anclem6 33620 fdc 33671 ismtyres 33737 isdrngo2 33887 rngohomco 33903 rngoisocnv 33910 dssmapnvod 38631 climxrrelem 40299 dvdsn1add 40472 dvnprodlem1 40479 stoweidlem27 40562 fourierdlem97 40738 qndenserrnbllem 40832 sge0iunmptlemfi 40948 |
Copyright terms: Public domain | W3C validator |