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

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

Proof of Theorem ad5ant14
StepHypRef Expression
1 ad5ant2.1 . . 3 ((𝜑𝜓) → 𝜒)
21adantlr 715 . 2 (((𝜑𝜃) ∧ 𝜓) → 𝜒)
32ad4ant13 751 1 (((((𝜑𝜃) ∧ 𝜏) ∧ 𝜓) ∧ 𝜂) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395
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 207  df-an 396
This theorem is referenced by:  leexp1a  14212  cpmatinvcl  22739  restcld  23196  ustuqtop3  24268  legval  28607  ccatws1f1o  32921  lssdimle  33635  zarcls1  33830  lindsenlbs  37602  matunitlindflem1  37603  modelaxrep  44946  xrralrecnnle  45333  limclner  45607  limsupub2  45768  xlimliminflimsup  45818  pimdecfgtioo  46673  pimincfltioo  46674
  Copyright terms: Public domain W3C validator