| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > 3adantr3 | Structured version Visualization version GIF version | ||
| Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 27-Apr-2005.) |
| Ref | Expression |
|---|---|
| 3adantr.1 | ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) |
| Ref | Expression |
|---|---|
| 3adantr3 | ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜏)) → 𝜃) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 3simpa 1149 | . 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜏) → (𝜓 ∧ 𝜒)) | |
| 2 | 3adantr.1 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) | |
| 3 | 1, 2 | sylan2 593 | 1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜏)) → 𝜃) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1087 |
| 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 df-3an 1089 |
| This theorem is referenced by: 3adant3r3 1185 3ad2antr1 1189 3ad2antr2 1190 sotr2 5626 dfwe2 7794 smogt 8407 infsupprpr 9544 wlogle 11796 fzadd2 13599 swrdspsleq 14703 tanadd 16203 prdssgrpd 18746 prdsmndd 18783 mhmmnd 19082 imasrng 20174 imasring 20327 prdslmodd 20967 sraassab 21888 mpllsslem 22020 scmatlss 22531 mdetunilem3 22620 ptclsg 23623 tmdgsum2 24104 isxmet2d 24337 xmetres2 24371 prdsxmetlem 24378 comet 24526 iimulcl 24966 icoopnst 24969 iocopnst 24970 icccvx 24981 dvfsumrlim 26072 dvfsumrlim2 26073 colhp 28778 eengtrkg 29001 wwlksnredwwlkn 29915 dmdsl3 32334 eqgvscpbl 33378 resconn 35251 poimirlem28 37655 poimirlem32 37659 broucube 37661 ftc1anclem7 37706 ftc1anc 37708 isdrngo2 37965 iscringd 38005 unichnidl 38038 lplnle 39542 2llnjN 39569 2lplnj 39622 osumcllem11N 39968 cdleme1 40229 erngplus2 40806 erngplus2-rN 40814 erngdvlem3 40992 erngdvlem3-rN 41000 dvaplusgv 41012 dvalveclem 41027 dvhvaddass 41099 dvhlveclem 41110 dihmeetlem12N 41320 issmflem 46742 fmtnoprmfac1 47552 lincresunit3lem2 48397 lincresunit3 48398 |
| Copyright terms: Public domain | W3C validator |