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

Theorem ad4ant124 1174
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 1119 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
32adantlr 714 1 ((((𝜑𝜓) ∧ 𝜏) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  w3a 1088
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 398  df-3an 1090
This theorem is referenced by:  ad5ant124  1366  ixxin  13341  odf1  19430  m2cpmfo  22258  cnflf  23506  cnfcf  23546  tmdmulg  23596  blin  23927  blsscls2  24013  metcn  24052  xrsxmet  24325  sqf11  26643  dimval  32686  dfgcd3  36205  lindsadd  36481  naddsuc2  42143  hspmbllem2  45343
  Copyright terms: Public domain W3C validator