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 483 | . 2 ⊢ ((𝜓 ∧ 𝜏) → 𝜓) | |
2 | adantl2.1 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) | |
3 | 1, 2 | sylanl2 677 | 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 208 df-an 397 |
This theorem is referenced by: disjxiun 5054 2ndconst 7785 oelim 8148 odi 8194 marypha1lem 8885 dfac12lem2 9558 infunsdom 9624 isf34lem4 9787 distrlem1pr 10435 lcmgcdlem 15938 lcmdvds 15940 drsdirfi 17536 isacs3lem 17764 conjnmzb 18331 psgndif 20674 frlmsslsp 20868 metss2lem 23048 nghmcn 23281 bndth 23489 itg2monolem1 24278 dvmptfsum 24499 ply1divex 24657 itgulm 24923 rpvmasumlem 25990 dchrmusum2 25997 dchrisum0lem2 26021 dchrisum0lem3 26022 mulog2sumlem2 26038 pntibndlem3 26095 wwlksubclwwlk 27764 blocni 28509 superpos 30058 chirredlem2 30095 eulerpartlemgvv 31533 ballotlemfc0 31649 ballotlemfcc 31650 bj-finsumval0 34455 pibt2 34580 fin2solem 34759 matunitlindflem1 34769 poimirlem28 34801 heicant 34808 ftc1anclem6 34853 ftc1anc 34856 fdc 34901 incsequz 34904 ismtyres 34967 isdrngo2 35117 rngohomco 35133 keridl 35191 linepsubN 36768 pmapsub 36784 mzpcompact2lem 39226 pellex 39310 monotuz 39416 unxpwdom3 39573 dssmapnvod 40244 radcnvrat 40523 fprodexp 41751 fprodabs2 41752 climxrrelem 41906 dvnprodlem1 42107 stoweidlem34 42196 fourierdlem42 42311 elaa2 42396 sge0iunmptlemfi 42572 aacllem 44830 |
Copyright terms: Public domain | W3C validator |