![]() |
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 1168 | 1 ⊢ ((𝜑 ∧ (𝜒 ∧ 𝜓 ∧ 𝜏)) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 ∧ w3a 1084 |
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 395 df-3an 1086 |
This theorem is referenced by: simpr1 1191 simpr1l 1227 simpr1r 1228 simpr11 1254 simpr12 1255 simpr13 1256 ispod 5603 funcnvqp 6623 dfwe2 7782 poxp 8142 cfcoflem 10315 axdc3lem 10493 fzadd2 13590 fzosubel2 13746 hashdifpr 14432 pfxccat3a 14746 sqrt0 15246 iscatd2 17694 funcestrcsetclem9 18172 funcsetcestrclem9 18187 curf2cl 18256 yonedalem4c 18302 grpsubadd 19022 mulgnnass 19103 mulgnn0ass 19104 dprdss 20029 dprd2da 20042 srgdilem 20175 lsssn0 20925 zntoslem 21554 sraassab 21865 psrbaglesuppOLD 21922 blsscls 24507 iimulcl 24951 pi1grplem 25067 pi1xfrf 25071 dvconst 25937 logexprlim 27254 wwlksnextbi 29828 clwwlkccatlem 29922 clwwlkccat 29923 umgr3cyclex 30116 nvss 30526 disjdsct 32614 idlsrgmnd 33389 issgon 33956 measdivcst 34057 measdivcstALTV 34058 prv1n 35259 elmrsubrn 35348 poimirlem28 37349 ftc1anc 37402 fdc 37446 cvrnbtwn3 38974 paddasslem9 39527 paddasslem17 39535 pmapjlln1 39554 lautj 39792 lautm 39793 dfsalgen2 45962 smflimlem4 46395 lidldomnnring 47613 funcringcsetcALTV2lem9 47675 funcringcsetclem9ALTV 47698 lincresunit3lem2 47863 isthincd2 48359 |
Copyright terms: Public domain | W3C validator |