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 717 | . 2 ⊢ ((𝜑 ∧ (𝜒 ∧ 𝜓)) → 𝜃) |
3 | 2 | 3adantr3 1173 | 1 ⊢ ((𝜑 ∧ (𝜒 ∧ 𝜓 ∧ 𝜏)) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∧ w3a 1089 |
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 210 df-an 400 df-3an 1091 |
This theorem is referenced by: simpr1 1196 simpr1l 1232 simpr1r 1233 simpr11 1259 simpr12 1260 simpr13 1261 ispod 5474 funcnvqp 6441 dfwe2 7556 poxp 7892 cfcoflem 9883 axdc3lem 10061 fzadd2 13144 fzosubel2 13299 hashdifpr 13979 pfxccat3a 14300 sqr0lem 14801 iscatd2 17181 funcestrcsetclem9 17652 funcsetcestrclem9 17667 curf2cl 17736 yonedalem4c 17782 grpsubadd 18448 mulgnnass 18523 mulgnn0ass 18524 dprdss 19413 dprd2da 19426 srgi 19523 lsssn0 19981 zntoslem 20518 psrbaglesuppOLD 20881 blsscls 23402 iimulcl 23831 pi1grplem 23943 pi1xfrf 23947 dvconst 24811 logexprlim 26103 wwlksnextbi 27975 clwwlkccatlem 28069 clwwlkccat 28070 umgr3cyclex 28263 nvss 28671 disjdsct 30752 idlsrgmnd 31370 issgon 31800 measdivcst 31901 measdivcstALTV 31902 prv1n 33103 elmrsubrn 33192 poimirlem28 35540 ftc1anc 35593 fdc 35638 cvrnbtwn3 37025 paddasslem9 37577 paddasslem17 37585 pmapjlln1 37604 lautj 37842 lautm 37843 dfsalgen2 43553 smflimlem4 43979 lidldomnnring 45159 funcringcsetcALTV2lem9 45273 funcringcsetclem9ALTV 45296 lincresunit3lem2 45492 isthincd2 45990 |
Copyright terms: Public domain | W3C validator |