![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ad5ant14 | 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 |
---|---|
ad5ant2.1 | ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
Ref | Expression |
---|---|
ad5ant14 | ⊢ (((((𝜑 ∧ 𝜃) ∧ 𝜏) ∧ 𝜓) ∧ 𝜂) → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ad5ant2.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | |
2 | 1 | adantlr 715 | . 2 ⊢ (((𝜑 ∧ 𝜃) ∧ 𝜓) → 𝜒) |
3 | 2 | ad4ant13 751 | 1 ⊢ (((((𝜑 ∧ 𝜃) ∧ 𝜏) ∧ 𝜓) ∧ 𝜂) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 |
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 207 df-an 396 |
This theorem is referenced by: leexp1a 14212 cpmatinvcl 22739 restcld 23196 ustuqtop3 24268 legval 28607 ccatws1f1o 32921 lssdimle 33635 zarcls1 33830 lindsenlbs 37602 matunitlindflem1 37603 modelaxrep 44946 xrralrecnnle 45333 limclner 45607 limsupub2 45768 xlimliminflimsup 45818 pimdecfgtioo 46673 pimincfltioo 46674 |
Copyright terms: Public domain | W3C validator |