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

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

Proof of Theorem ad4ant124
StepHypRef Expression
1 ad4ant3.1 . . 3 ((𝜑𝜓𝜒) → 𝜃)
213expa 1118 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
32adantlr 713 1 ((((𝜑𝜓) ∧ 𝜏) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1087
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 206  df-an 397  df-3an 1089
This theorem is referenced by:  ad5ant124  1365  ixxin  13337  odf1  19424  m2cpmfo  22249  cnflf  23497  cnfcf  23537  tmdmulg  23587  blin  23918  blsscls2  24004  metcn  24043  xrsxmet  24316  sqf11  26632  dimval  32674  dfgcd3  36193  lindsadd  36469  naddsuc2  42128  hspmbllem2  45329
  Copyright terms: Public domain W3C validator