![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > adantlrr | 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 |
---|---|
adantlrr | ⊢ (((𝜑 ∧ (𝜓 ∧ 𝜏)) ∧ 𝜒) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl 484 | . 2 ⊢ ((𝜓 ∧ 𝜏) → 𝜓) | |
2 | adantl2.1 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) | |
3 | 1, 2 | sylanl2 680 | 1 ⊢ (((𝜑 ∧ (𝜓 ∧ 𝜏)) ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 |
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 398 |
This theorem is referenced by: disjxiun 5103 2ndconst 8034 oelim 8481 odi 8527 marypha1lem 9370 dfac12lem2 10081 infunsdom 10151 isf34lem4 10314 distrlem1pr 10962 lcmgcdlem 16483 lcmdvds 16485 drsdirfi 18195 isacs3lem 18432 conjnmzb 19044 psgndif 21009 frlmsslsp 21205 metss2lem 23870 nghmcn 24112 bndth 24324 itg2monolem1 25118 dvmptfsum 25342 ply1divex 25504 itgulm 25770 rpvmasumlem 26838 dchrmusum2 26845 dchrisum0lem2 26869 dchrisum0lem3 26870 mulog2sumlem2 26886 pntibndlem3 26943 wwlksubclwwlk 29005 blocni 29750 superpos 31299 chirredlem2 31336 eulerpartlemgvv 32979 ballotlemfc0 33095 ballotlemfcc 33096 bj-finsumval0 35759 pibt2 35891 fin2solem 36067 matunitlindflem1 36077 poimirlem28 36109 heicant 36116 ftc1anclem6 36159 ftc1anc 36162 fdc 36207 incsequz 36210 ismtyres 36270 isdrngo2 36420 rngohomco 36436 keridl 36494 linepsubN 38218 pmapsub 38234 fsuppind 40768 mhpind 40772 mzpcompact2lem 41077 pellex 41161 monotuz 41268 unxpwdom3 41425 cantnfresb 41661 dssmapnvod 42299 radcnvrat 42601 fprodexp 43842 fprodabs2 43843 climxrrelem 43997 dvnprodlem1 44194 stoweidlem34 44282 fourierdlem42 44397 elaa2 44482 sge0iunmptlemfi 44661 aacllem 47255 |
Copyright terms: Public domain | W3C validator |