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 693 . 2 (((𝜃𝜑) ∧ 𝜓) → 𝜒)
32adantlr 694 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  14033  matunitlindflem1  33738  matunitlindflem2  33739  founiiun0  39897  xralrple2  40086  rexabslelem  40161  climisp  40496  climxrre  40500  cnrefiisplem  40573  sge0iunmptlemre  41149  nnfoctbdjlem  41189  iundjiun  41194  meaiuninc3v  41218  hoidmvlelem3  41331  hspmbllem2  41361  smflimlem2  41500
  Copyright terms: Public domain W3C validator