![]() |
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 481 | . 2 ⊢ ((𝜓 ∧ 𝜏) → 𝜓) | |
2 | adantl2.1 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) | |
3 | 1, 2 | sylanl2 679 | 1 ⊢ (((𝜑 ∧ (𝜓 ∧ 𝜏)) ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 |
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 395 |
This theorem is referenced by: disjxiun 5146 2ndconst 8106 oelim 8555 odi 8600 marypha1lem 9458 dfac12lem2 10169 infunsdom 10239 isf34lem4 10402 distrlem1pr 11050 lcmgcdlem 16580 lcmdvds 16582 drsdirfi 18300 isacs3lem 18537 conjnmzb 19216 psgndif 21551 frlmsslsp 21747 metss2lem 24464 nghmcn 24706 bndth 24928 itg2monolem1 25724 dvmptfsum 25951 ply1divex 26117 itgulm 26389 rpvmasumlem 27465 dchrmusum2 27472 dchrisum0lem2 27496 dchrisum0lem3 27497 mulog2sumlem2 27513 pntibndlem3 27570 wwlksubclwwlk 29940 blocni 30687 superpos 32236 chirredlem2 32273 eulerpartlemgvv 34127 ballotlemfc0 34243 ballotlemfcc 34244 bj-finsumval0 36895 pibt2 37027 fin2solem 37210 matunitlindflem1 37220 poimirlem28 37252 heicant 37259 ftc1anclem6 37302 ftc1anc 37305 fdc 37349 incsequz 37352 ismtyres 37412 isdrngo2 37562 rngohomco 37578 keridl 37636 linepsubN 39355 pmapsub 39371 fsuppind 41958 mhpind 41962 mzpcompact2lem 42313 pellex 42397 monotuz 42504 unxpwdom3 42661 cantnfresb 42895 dssmapnvod 43592 radcnvrat 43893 fprodexp 45120 fprodabs2 45121 climxrrelem 45275 dvnprodlem1 45472 stoweidlem34 45560 fourierdlem42 45675 elaa2 45760 sge0iunmptlemfi 45939 aacllem 48420 |
Copyright terms: Public domain | W3C validator |