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

Theorem ad5ant24 761
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  8615  cofsmo  10307  leexp1a  14212  natpropd  18033  mhpmulcl  22171  isucn2  24304  metust  24587  hpgerlem  28788  clwlkclwwlklem2a4  30026  cyc3genpm  33155  nsgqusf1olem1  33421  1arithufdlem2  33553  ist0cld  33794  matunitlindflem1  37603  rexabslelem  45368
  Copyright terms: Public domain W3C validator