![]() |
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 1118 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) |
3 | 2 | 3adantr2 1168 | 1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1085 |
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 396 df-3an 1087 |
This theorem is referenced by: plttr 18328 latjlej2 18440 latmlem1 18455 latmlem2 18456 latledi 18463 latmlej11 18464 latmlej12 18465 ipopos 18522 grppnpcan2 18984 mulgsubdir 19063 imasrng 20111 imasring 20260 isdomn4 21244 zntoslem 21484 mettri2 24241 mettri 24252 xmetrtri 24255 xmetrtri2 24256 metrtri 24257 ablomuldiv 30356 ablonnncan1 30361 nvmdi 30452 dipdi 30647 dipassr 30650 dipsubdir 30652 dipsubdi 30653 btwncomim 35604 cgr3tr4 35643 cgr3rflx 35645 colinbtwnle 35709 rngosubdi 37413 rngosubdir 37414 dmncan1 37544 dmncan2 37545 omlfh1N 38725 omlfh3N 38726 cvrnbtwn3 38743 cvrnbtwn4 38746 cvrcmp2 38751 hlatjrot 38840 cvrat3 38910 lplnribN 39019 ltrn2ateq 39648 dvalveclem 40493 mendlmod 42608 |
Copyright terms: Public domain | W3C validator |