![]() |
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 485 | . 2 ⊢ ((𝜏 ∧ 𝜓) → 𝜓) | |
2 | adantl2.1 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) | |
3 | 1, 2 | sylanl2 679 | 1 ⊢ (((𝜑 ∧ (𝜏 ∧ 𝜓)) ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 |
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 206 df-an 397 |
This theorem is referenced by: 1stconst 8024 omlimcl 8517 odi 8518 oelim2 8534 mapxpen 9045 unwdomg 9478 dfac12lem2 10038 infunsdom 10108 fin1a2s 10308 ccatpfx 14543 frlmup1 21151 fbasrn 23181 lmmbr 24568 grporcan 29305 unoplin 30707 hmoplin 30729 superpos 31141 ccatf1 31647 subfacp1lem5 33606 matunitlindflem1 36006 poimirlem4 36014 itg2addnclem 36061 ftc1anclem6 36088 fdc 36136 ismtyres 36199 isdrngo2 36349 rngohomco 36365 rngoisocnv 36372 dssmapnvod 42197 climxrrelem 43885 dvdsn1add 44075 dvnprodlem1 44082 stoweidlem27 44163 fourierdlem97 44339 qndenserrnbllem 44430 sge0iunmptlemfi 44549 |
Copyright terms: Public domain | W3C validator |