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 716 | 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 206 df-an 397 |
This theorem is referenced by: ad5ant14 755 ad5ant24 758 fntpb 7085 peano5 7740 peano5OLD 7741 f1o2ndf1 7963 cantnfle 9429 cantnflem1c 9445 ttukeylem5 10269 rlimsqzlem 15360 dvdslcmf 16336 poslubmo 18129 posglbmo 18130 smndex1mgm 18546 isgrpinv 18632 ghmgrp 18699 dprdfcntz 19618 cply1coe0bi 21471 isnrm3 22510 cnextcn 23218 ustexsym 23367 ustex2sym 23368 ustex3sym 23369 trust 23381 fmucnd 23444 trcfilu 23446 metust 23714 cxpmul2z 25846 umgrres1lem 27677 upgrres1 27680 friendshipgt3 28762 ccatf1 31223 cyc3evpm 31417 znfermltl 31562 rhmimaidl 31609 txomap 31784 zart0 31829 repr0 32591 breprexplemc 32612 hgt750lemb 32636 satffunlem1lem2 33365 satffunlem2lem2 33368 lindsadd 35770 matunitlindflem1 35773 mapss2 42745 supxrge 42877 xrlexaddrp 42891 infxr 42906 infleinf 42911 unb2ltle 42955 supminfxr 43004 limsuppnfdlem 43242 limsupub 43245 limsuppnflem 43251 climinf3 43257 limsupmnflem 43261 climxrre 43291 liminfvalxr 43324 fperdvper 43460 sge0isum 43965 sge0gtfsumgt 43981 sge0seq 43984 nnfoctbdjlem 43993 meaiuninc3v 44022 omeiunltfirp 44057 hspdifhsp 44154 hspmbllem2 44165 pimdecfgtioo 44254 pimincfltioo 44255 preimageiingt 44257 preimaleiinlt 44258 smfid 44288 proththd 45066 |
Copyright terms: Public domain | W3C validator |