MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ad5ant15 Structured version   Visualization version   GIF version

Theorem ad5ant15 758
Description: Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
Hypothesis
Ref Expression
ad5ant2.1 ((𝜑𝜓) → 𝜒)
Assertion
Ref Expression
ad5ant15 (((((𝜑𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜓) → 𝜒)

Proof of Theorem ad5ant15
StepHypRef Expression
1 ad5ant2.1 . . 3 ((𝜑𝜓) → 𝜒)
21adantlr 714 . 2 (((𝜑𝜃) ∧ 𝜓) → 𝜒)
32ad4ant14 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