![]() |
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 |
---|---|
3exp.1 | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
3adant3r2 | ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3exp.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
2 | 1 | 3expb 1285 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) |
3 | 2 | 3adantr2 1241 | 1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∧ w3a 1054 |
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 197 df-an 385 df-3an 1056 |
This theorem is referenced by: plttr 17017 latjlej2 17113 latmlem1 17128 latmlem2 17129 latledi 17136 latmlej11 17137 latmlej12 17138 ipopos 17207 grppnpcan2 17556 mulgsubdir 17629 imasring 18665 zntoslem 19953 mettri2 22193 mettri 22204 xmetrtri 22207 xmetrtri2 22208 metrtri 22209 ablomuldiv 27534 ablonnncan1 27540 nvmdi 27631 dipdi 27826 dipassr 27829 dipsubdir 27831 dipsubdi 27832 btwncomim 32245 cgr3tr4 32284 cgr3rflx 32286 colinbtwnle 32350 rngosubdi 33874 rngosubdir 33875 dmncan1 34005 dmncan2 34006 omlfh1N 34863 omlfh3N 34864 cvrnbtwn3 34881 cvrnbtwn4 34884 cvrcmp2 34889 hlatjrot 34977 cvrat3 35046 lplnribN 35155 ltrn2ateq 35785 dvalveclem 36631 mendlmod 38080 |
Copyright terms: Public domain | W3C validator |