![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ad4ant13 | Structured version Visualization version GIF version |
Description: Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.) |
Ref | Expression |
---|---|
ad4ant2.1 | ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
Ref | Expression |
---|---|
ad4ant13 | ⊢ ((((𝜑 ∧ 𝜃) ∧ 𝜓) ∧ 𝜏) → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ad4ant2.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | |
2 | 1 | adantr 481 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜏) → 𝜒) |
3 | 2 | adantllr 715 | 1 ⊢ ((((𝜑 ∧ 𝜃) ∧ 𝜓) ∧ 𝜏) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 |
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 208 df-an 397 |
This theorem is referenced by: ad5ant14 754 ad5ant24 757 fntpb 6838 peano5 7461 f1o2ndf1 7671 cantnfle 8980 cantnflem1c 8996 ttukeylem5 9781 rlimsqzlem 14839 dvdslcmf 15804 poslubmo 17585 posglbmo 17586 isgrpinv 17913 ghmgrp 17980 dprdfcntz 18854 cply1coe0bi 20151 isnrm3 21651 cnextcn 22359 ustexsym 22507 ustex2sym 22508 ustex3sym 22509 trust 22521 fmucnd 22584 trcfilu 22586 metust 22851 cxpmul2z 24955 umgrres1lem 26775 upgrres1 26778 friendshipgt3 27869 cyc3evpm 30430 repr0 31499 breprexplemc 31520 hgt750lemb 31544 satffunlem1lem2 32258 satffunlem2lem2 32261 lindsadd 34416 matunitlindflem1 34419 mapss2 41008 supxrge 41147 xrlexaddrp 41161 infxr 41176 infleinf 41181 unb2ltle 41231 supminfxr 41282 limsuppnfdlem 41524 limsupub 41527 limsuppnflem 41533 climinf3 41539 limsupmnflem 41543 climxrre 41573 liminfvalxr 41606 fperdvper 41744 sge0isum 42251 sge0gtfsumgt 42267 sge0seq 42270 nnfoctbdjlem 42279 meaiuninc3v 42308 omeiunltfirp 42343 hspdifhsp 42440 hspmbllem2 42451 pimdecfgtioo 42537 pimincfltioo 42538 preimageiingt 42540 preimaleiinlt 42541 smfid 42571 proththd 43261 |
Copyright terms: Public domain | W3C validator |