![]() |
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 | adantlr 707 | . 2 ⊢ (((𝜑 ∧ 𝜃) ∧ 𝜓) → 𝜒) |
3 | 2 | adantr 473 | 1 ⊢ ((((𝜑 ∧ 𝜃) ∧ 𝜓) ∧ 𝜏) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 385 |
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 386 |
This theorem is referenced by: ad5ant14 770 ad5ant24 776 fntpb 6701 dvdslcmf 15676 poslubmo 17458 posglbmo 17459 trust 22358 metust 22688 umgrres1lem 26537 upgrres1 26540 friendshipgt3 27776 repr0 31202 breprexplemc 31223 hgt750lemb 31247 matunitlindflem1 33887 mapss2 40138 supxrge 40287 xrlexaddrp 40301 infxr 40316 infleinf 40321 unb2ltle 40374 supminfxr 40426 limsuppnfdlem 40666 limsupub 40669 limsuppnflem 40675 climinf3 40681 limsupmnflem 40685 climxrre 40715 liminfvalxr 40748 fperdvper 40866 sge0isum 41376 sge0gtfsumgt 41392 sge0seq 41395 nnfoctbdjlem 41404 meaiuninc3v 41433 omeiunltfirp 41468 hspdifhsp 41565 hspmbllem2 41576 pimdecfgtioo 41662 pimincfltioo 41663 preimageiingt 41665 preimaleiinlt 41666 smfid 41696 proththd 42302 |
Copyright terms: Public domain | W3C validator |