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

Theorem ad5ant14 756
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
ad5ant14 (((((𝜑𝜃) ∧ 𝜏) ∧ 𝜓) ∧ 𝜂) → 𝜒)

Proof of Theorem ad5ant14
StepHypRef Expression
1 ad5ant2.1 . . 3 ((𝜑𝜓) → 𝜒)
21adantlr 713 . 2 (((𝜑𝜃) ∧ 𝜓) → 𝜒)
32ad4ant13 749 1 (((((𝜑𝜃) ∧ 𝜏) ∧ 𝜓) ∧ 𝜂) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 397
This theorem is referenced by:  leexp1a  14077  cpmatinvcl  22062  restcld  22519  ustuqtop3  23591  legval  27424  lssdimle  32196  zarcls1  32341  lindsenlbs  36062  matunitlindflem1  36063  xrralrecnnle  43591  limclner  43862  limsupub2  44023  xlimliminflimsup  44073  pimdecfgtioo  44928  pimincfltioo  44929
  Copyright terms: Public domain W3C validator