![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ad5ant15 | 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 |
---|---|
ad5ant15 | ⊢ (((((𝜑 ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜓) → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ad5ant2.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | |
2 | 1 | adantlr 714 | . 2 ⊢ (((𝜑 ∧ 𝜃) ∧ 𝜓) → 𝜒) |
3 | 2 | ad4ant14 751 | 1 ⊢ (((((𝜑 ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜓) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 |
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 398 |
This theorem is referenced by: summolem2 15662 ntrivcvg 15843 xkoccn 23123 abelthlem8 25951 rpvmasum2 27015 mulog2sumlem2 27038 f1otrge 28123 nn0xmulclb 31984 intlidl 32536 ply1degltdimlem 32707 fedgmul 32716 signstfvneq0 33583 breprexplemc 33644 mblfinlem2 36526 supxrgelem 44047 supxrge 44048 rexabslelem 44128 uzub 44141 smflimlem4 45490 |
Copyright terms: Public domain | W3C validator |