|   | 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 484 | . 2 ⊢ ((𝜏 ∧ 𝜓) → 𝜓) | |
| 2 | adantl2.1 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) | |
| 3 | 1, 2 | sylanl2 681 | 1 ⊢ (((𝜑 ∧ (𝜏 ∧ 𝜓)) ∧ 𝜒) → 𝜃) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∧ wa 395 | 
| 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 207 df-an 396 | 
| This theorem is referenced by: 1stconst 8125 omlimcl 8616 odi 8617 oelim2 8633 mapxpen 9183 unwdomg 9624 dfac12lem2 10185 infunsdom 10253 fin1a2s 10454 ccatpfx 14739 frlmup1 21818 fbasrn 23892 lmmbr 25292 grporcan 30537 unoplin 31939 hmoplin 31961 superpos 32373 ccatf1 32933 subfacp1lem5 35189 matunitlindflem1 37623 poimirlem4 37631 itg2addnclem 37678 ftc1anclem6 37705 fdc 37752 ismtyres 37815 isdrngo2 37965 rngohomco 37981 rngoisocnv 37988 dssmapnvod 44033 climxrrelem 45764 dvdsn1add 45954 dvnprodlem1 45961 stoweidlem27 46042 fourierdlem97 46218 qndenserrnbllem 46309 sge0iunmptlemfi 46428 | 
| Copyright terms: Public domain | W3C validator |