![]() |
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 711 | . 2 ⊢ (((𝜑 ∧ 𝜃) ∧ 𝜓) → 𝜒) |
3 | 2 | ad4ant14 748 | 1 ⊢ (((((𝜑 ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜓) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 |
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 395 |
This theorem is referenced by: summolem2 15666 ntrivcvg 15847 xkoccn 23343 abelthlem8 26187 rpvmasum2 27251 mulog2sumlem2 27274 f1otrge 28390 nn0xmulclb 32251 intlidl 32810 ply1degltdimlem 32995 fedgmul 33004 signstfvneq0 33881 breprexplemc 33942 mblfinlem2 36829 supxrgelem 44345 supxrge 44346 rexabslelem 44426 uzub 44439 smflimlem4 45788 |
Copyright terms: Public domain | W3C validator |