| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > 3adant3r1 | Structured version Visualization version GIF version | ||
| Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Feb-2008.) |
| Ref | Expression |
|---|---|
| ad4ant3.1 | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
| Ref | Expression |
|---|---|
| 3adant3r1 | ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓 ∧ 𝜒)) → 𝜃) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ad4ant3.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
| 2 | 1 | 3expb 1121 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) |
| 3 | 2 | 3adantr1 1170 | 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: dif1en 9200 ccatswrd 14706 plttr 18387 pltletr 18388 latjlej1 18498 latjlej2 18499 latnlej 18501 latnlej2 18504 latmlem2 18515 latledi 18522 latjass 18528 latj32 18530 latj13 18531 ipopos 18581 tsrlemax 18631 imasmnd2 18787 grpsubsub 19047 grpnnncan2 19055 imasgrp2 19073 mulgnn0ass 19128 mulgsubdir 19132 cmn32 19818 ablsubadd 19827 imasrng 20174 imasring 20327 isdomn4 20716 zntoslem 21575 xmettri3 24363 mettri3 24364 xmetrtri 24365 xmetrtri2 24366 metrtri 24367 cphdivcl 25216 cphassr 25246 relogbmulexp 26821 grpodivdiv 30559 grpomuldivass 30560 ablo32 30568 ablodivdiv4 30573 ablodiv32 30574 nvmdi 30667 dipdi 30862 dipassr 30865 dipsubdir 30867 dipsubdi 30868 dvrcan5 33240 cgr3tr4 36053 cgr3rflx 36055 endofsegid 36086 seglemin 36114 broutsideof2 36123 rngosubdi 37952 rngosubdir 37953 isdrngo2 37965 crngm23 38009 dmncan2 38084 latmassOLD 39230 latm32 39232 cvrnbtwn4 39280 cvrcmp2 39285 ltcvrntr 39426 atcvrj0 39430 3dim3 39471 paddasslem17 39838 paddass 39840 lautlt 40093 lautcvr 40094 lautj 40095 lautm 40096 erngdvlem3 40992 dvalveclem 41027 mendlmod 43201 |
| Copyright terms: Public domain | W3C validator |