![]() |
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 715 | . 2 ⊢ ((𝜑 ∧ (𝜒 ∧ 𝜓)) → 𝜃) |
3 | 2 | 3adantr3 1171 | 1 ⊢ ((𝜑 ∧ (𝜒 ∧ 𝜓 ∧ 𝜏)) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ 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 206 df-an 397 df-3an 1089 |
This theorem is referenced by: simpr1 1194 simpr1l 1230 simpr1r 1231 simpr11 1257 simpr12 1258 simpr13 1259 ispod 5552 funcnvqp 6562 dfwe2 7700 poxp 8052 cfcoflem 10166 axdc3lem 10344 fzadd2 13430 fzosubel2 13586 hashdifpr 14269 pfxccat3a 14580 sqrt0 15080 iscatd2 17515 funcestrcsetclem9 17990 funcsetcestrclem9 18005 curf2cl 18074 yonedalem4c 18120 grpsubadd 18788 mulgnnass 18864 mulgnn0ass 18865 dprdss 19761 dprd2da 19774 srgdilem 19876 lsssn0 20355 zntoslem 20910 psrbaglesuppOLD 21274 blsscls 23809 iimulcl 24246 pi1grplem 24358 pi1xfrf 24362 dvconst 25227 logexprlim 26519 wwlksnextbi 28684 clwwlkccatlem 28778 clwwlkccat 28779 umgr3cyclex 28972 nvss 29380 disjdsct 31459 idlsrgmnd 32094 issgon 32550 measdivcst 32651 measdivcstALTV 32652 prv1n 33853 elmrsubrn 33942 poimirlem28 36038 ftc1anc 36091 fdc 36136 cvrnbtwn3 37670 paddasslem9 38223 paddasslem17 38231 pmapjlln1 38250 lautj 38488 lautm 38489 dfsalgen2 44477 smflimlem4 44910 lidldomnnring 46123 funcringcsetcALTV2lem9 46237 funcringcsetclem9ALTV 46260 lincresunit3lem2 46456 isthincd2 46953 |
Copyright terms: Public domain | W3C validator |