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  14215  cpmatinvcl  22723  restcld  23180  ustuqtop3  24252  legval  28592  ccatws1f1o  32936  lssdimle  33658  zarcls1  33868  lindsenlbs  37622  matunitlindflem1  37623  modelaxrep  44998  xrralrecnnle  45394  limclner  45666  limsupub2  45827  xlimliminflimsup  45877  pimdecfgtioo  46732  pimincfltioo  46733
  Copyright terms: Public domain W3C validator