![]() |
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 716 | . 2 ⊢ ((𝜑 ∧ (𝜒 ∧ 𝜓)) → 𝜃) |
3 | 2 | 3adantr3 1172 | 1 ⊢ ((𝜑 ∧ (𝜒 ∧ 𝜓 ∧ 𝜏)) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 ∧ w3a 1088 |
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 398 df-3an 1090 |
This theorem is referenced by: simpr1 1195 simpr1l 1231 simpr1r 1232 simpr11 1258 simpr12 1259 simpr13 1260 ispod 5555 funcnvqp 6566 dfwe2 7709 poxp 8061 cfcoflem 10209 axdc3lem 10387 fzadd2 13477 fzosubel2 13633 hashdifpr 14316 pfxccat3a 14627 sqrt0 15127 iscatd2 17562 funcestrcsetclem9 18037 funcsetcestrclem9 18052 curf2cl 18121 yonedalem4c 18167 grpsubadd 18836 mulgnnass 18912 mulgnn0ass 18913 dprdss 19809 dprd2da 19822 srgdilem 19924 lsssn0 20411 zntoslem 20966 psrbaglesuppOLD 21330 blsscls 23866 iimulcl 24303 pi1grplem 24415 pi1xfrf 24419 dvconst 25284 logexprlim 26576 wwlksnextbi 28842 clwwlkccatlem 28936 clwwlkccat 28937 umgr3cyclex 29130 nvss 29538 disjdsct 31619 idlsrgmnd 32259 issgon 32725 measdivcst 32826 measdivcstALTV 32827 prv1n 34028 elmrsubrn 34117 poimirlem28 36109 ftc1anc 36162 fdc 36207 cvrnbtwn3 37741 paddasslem9 38294 paddasslem17 38302 pmapjlln1 38321 lautj 38559 lautm 38560 dfsalgen2 44589 smflimlem4 45022 lidldomnnring 46235 funcringcsetcALTV2lem9 46349 funcringcsetclem9ALTV 46372 lincresunit3lem2 46568 isthincd2 47065 |
Copyright terms: Public domain | W3C validator |