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

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

Proof of Theorem ad5ant24
StepHypRef Expression
1 ad5ant2.1 . . 3 ((𝜑𝜓) → 𝜒)
21adantll 714 . 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:  omlimcl  8617  cofsmo  10310  leexp1a  14216  natpropd  18025  mhpmulcl  22154  isucn2  24289  metust  24572  hpgerlem  28774  clwlkclwwlklem2a4  30017  cyc3genpm  33173  nsgqusf1olem1  33442  1arithufdlem2  33574  ist0cld  33833  matunitlindflem1  37624  rexabslelem  45434
  Copyright terms: Public domain W3C validator