Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 3ad2antr1 | Structured version Visualization version GIF version |
Description: Deduction adding conjuncts to antecedent. (Contributed by NM, 25-Dec-2007.) |
Ref | Expression |
---|---|
3ad2antl.1 | ⊢ ((𝜑 ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
3ad2antr1 | ⊢ ((𝜑 ∧ (𝜒 ∧ 𝜓 ∧ 𝜏)) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3ad2antl.1 | . . 3 ⊢ ((𝜑 ∧ 𝜒) → 𝜃) | |
2 | 1 | adantrr 713 | . 2 ⊢ ((𝜑 ∧ (𝜒 ∧ 𝜓)) → 𝜃) |
3 | 2 | 3adantr3 1163 | 1 ⊢ ((𝜑 ∧ (𝜒 ∧ 𝜓 ∧ 𝜏)) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1079 |
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 208 df-an 397 df-3an 1081 |
This theorem is referenced by: simpr1 1186 simpr1l 1222 simpr1r 1223 simpr11 1249 simpr12 1250 simpr13 1251 ispod 5475 funcnvqp 6411 dfwe2 7485 poxp 7811 cfcoflem 9682 axdc3lem 9860 fzadd2 12930 fzosubel2 13085 hashdifpr 13764 pfxccat3a 14088 sqr0lem 14588 iscatd2 16940 funcestrcsetclem9 17386 funcsetcestrclem9 17401 curf2cl 17469 yonedalem4c 17515 grpsubadd 18125 mulgnnass 18200 mulgnn0ass 18201 dprdss 19080 dprd2da 19093 srgi 19190 lsssn0 19648 psrbaglesupp 20076 zntoslem 20631 blsscls 23044 iimulcl 23468 pi1grplem 23580 pi1xfrf 23584 dvconst 24441 logexprlim 25728 wwlksnextbi 27599 clwwlkccatlem 27694 clwwlkccat 27695 umgr3cyclex 27889 nvss 28297 disjdsct 30364 issgon 31281 measdivcst 31382 measdivcstALTV 31383 prv1n 32575 elmrsubrn 32664 poimirlem28 34801 ftc1anc 34856 fdc 34901 cvrnbtwn3 36292 paddasslem9 36844 paddasslem17 36852 pmapjlln1 36871 lautj 37109 lautm 37110 dfsalgen2 42501 smflimlem4 42927 lidldomnnring 44129 funcringcsetcALTV2lem9 44243 funcringcsetclem9ALTV 44266 lincresunit3lem2 44463 |
Copyright terms: Public domain | W3C validator |