![]() |
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 704 | . 2 ⊢ ((𝜑 ∧ (𝜒 ∧ 𝜓)) → 𝜃) |
3 | 2 | 3adantr3 1151 | 1 ⊢ ((𝜑 ∧ (𝜒 ∧ 𝜓 ∧ 𝜏)) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 387 ∧ w3a 1068 |
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 199 df-an 388 df-3an 1070 |
This theorem is referenced by: simpr1 1174 simpr1l 1210 simpr1r 1211 simpr11 1237 simpr12 1238 simpr13 1239 ispod 5327 funcnvqp 6245 dfwe2 7306 poxp 7620 cfcoflem 9484 axdc3lem 9662 fzadd2 12751 fzosubel2 12905 hashdifpr 13580 pfxccat3a 13932 sqr0lem 14451 iscatd2 16800 funcestrcsetclem9 17246 funcsetcestrclem9 17261 curf2cl 17329 yonedalem4c 17375 grpsubadd 17964 mulgnnass 18036 mulgnn0ass 18037 dprdss 18891 dprd2da 18904 srgi 18974 lsssn0 19431 psrbaglesupp 19852 zntoslem 20395 blsscls 22810 iimulcl 23234 pi1grplem 23346 pi1xfrf 23350 dvconst 24207 logexprlim 25493 wwlksnextbi 27372 wwlksnextbiOLD 27373 umgr3cyclex 27702 nvss 28137 disjdsct 30179 issgon 30984 measdivcstOLD 31085 measdivcst 31086 elmrsubrn 32227 poimirlem28 34309 ftc1anc 34364 fdc 34410 cvrnbtwn3 35805 paddasslem9 36357 paddasslem17 36365 pmapjlln1 36384 lautj 36622 lautm 36623 dfsalgen2 42001 smflimlem4 42427 lidldomnnring 43505 funcringcsetcALTV2lem9 43619 funcringcsetclem9ALTV 43642 lincresunit3lem2 43842 |
Copyright terms: Public domain | W3C validator |