|   | 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 482 | . 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: disjxiun 5139 2ndconst 8127 oelim 8573 odi 8618 marypha1lem 9474 dfac12lem2 10186 infunsdom 10254 isf34lem4 10418 distrlem1pr 11066 lcmgcdlem 16644 lcmdvds 16646 drsdirfi 18352 isacs3lem 18588 conjnmzb 19272 psgndif 21621 frlmsslsp 21817 metss2lem 24525 nghmcn 24767 bndth 24991 itg2monolem1 25786 dvmptfsum 26014 ply1divex 26177 itgulm 26452 rpvmasumlem 27532 dchrmusum2 27539 dchrisum0lem2 27563 dchrisum0lem3 27564 mulog2sumlem2 27580 pntibndlem3 27637 wwlksubclwwlk 30078 blocni 30825 superpos 32374 chirredlem2 32411 eulerpartlemgvv 34379 ballotlemfc0 34496 ballotlemfcc 34497 bj-finsumval0 37287 pibt2 37419 fin2solem 37614 matunitlindflem1 37624 poimirlem28 37656 heicant 37663 ftc1anclem6 37706 ftc1anc 37709 fdc 37753 incsequz 37756 ismtyres 37816 isdrngo2 37966 rngohomco 37982 keridl 38040 linepsubN 39755 pmapsub 39771 fsuppind 42605 mhpind 42609 mzpcompact2lem 42767 pellex 42851 monotuz 42958 unxpwdom3 43112 cantnfresb 43342 dssmapnvod 44038 radcnvrat 44338 fprodexp 45614 fprodabs2 45615 climxrrelem 45769 dvnprodlem1 45966 stoweidlem34 46054 fourierdlem42 46169 elaa2 46254 sge0iunmptlemfi 46433 aacllem 49375 | 
| Copyright terms: Public domain | W3C validator |