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

Theorem ad4ant24 1212
Description: Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
Hypothesis
Ref Expression
ad4ant2.1 ((𝜑𝜓) → 𝜒)
Assertion
Ref Expression
ad4ant24 ((((𝜃𝜑) ∧ 𝜏) ∧ 𝜓) → 𝜒)

Proof of Theorem ad4ant24
StepHypRef Expression
1 ad4ant2.1 . . 3 ((𝜑𝜓) → 𝜒)
21adantll 685 . 2 (((𝜃𝜑) ∧ 𝜓) → 𝜒)
32adantlr 686 1 ((((𝜃𝜑) ∧ 𝜏) ∧ 𝜓) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 197  df-an 383
This theorem is referenced by:  seqshft  14032  matunitlindflem1  33734  matunitlindflem2  33735  founiiun0  39893  xralrple2  40082  rexabslelem  40157  climisp  40492  climxrre  40496  cnrefiisplem  40569  sge0iunmptlemre  41145  nnfoctbdjlem  41185  iundjiun  41190  meaiuninc3v  41214  hoidmvlelem3  41327  hspmbllem2  41357  smflimlem2  41496
  Copyright terms: Public domain W3C validator