| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > 3adant3r2 | Structured version Visualization version GIF version | ||
| Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 17-Feb-2008.) |
| Ref | Expression |
|---|---|
| ad4ant3.1 | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
| Ref | Expression |
|---|---|
| 3adant3r2 | ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ad4ant3.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
| 2 | 1 | 3expb 1121 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) |
| 3 | 2 | 3adantr2 1171 | 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: plttr 18387 latjlej2 18499 latmlem1 18514 latmlem2 18515 latledi 18522 latmlej11 18523 latmlej12 18524 ipopos 18581 grppnpcan2 19052 mulgsubdir 19132 imasrng 20174 imasring 20327 isdomn4 20716 zntoslem 21575 mettri2 24351 mettri 24362 xmetrtri 24365 xmetrtri2 24366 metrtri 24367 ablomuldiv 30571 ablonnncan1 30576 nvmdi 30667 dipdi 30862 dipassr 30865 dipsubdir 30867 dipsubdi 30868 btwncomim 36014 cgr3tr4 36053 cgr3rflx 36055 colinbtwnle 36119 rngosubdi 37952 rngosubdir 37953 dmncan1 38083 dmncan2 38084 omlfh1N 39259 omlfh3N 39260 cvrnbtwn3 39277 cvrnbtwn4 39280 cvrcmp2 39285 hlatjrot 39374 cvrat3 39444 lplnribN 39553 ltrn2ateq 40182 dvalveclem 41027 mendlmod 43201 |
| Copyright terms: Public domain | W3C validator |