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 713 | . 2 ⊢ (((𝜑 ∧ 𝜃) ∧ 𝜓) → 𝜒) |
3 | 2 | ad4ant14 750 | 1 ⊢ (((((𝜑 ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜓) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 |
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 209 df-an 399 |
This theorem is referenced by: summolem2 15075 ntrivcvg 15255 xkoccn 22229 abelthlem8 25029 rpvmasum2 26090 mulog2sumlem2 26113 f1otrge 26660 nn0xmulclb 30498 fedgmul 31029 signstfvneq0 31844 breprexplemc 31905 mblfinlem2 34932 supxrgelem 41612 supxrge 41613 rexabslelem 41699 uzub 41712 smflimlem4 43057 |
Copyright terms: Public domain | W3C validator |