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

Theorem ad4ant124 1167
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 1112 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
32adantlr 711 1 ((((𝜑𝜓) ∧ 𝜏) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1081
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 208  df-an 397  df-3an 1083
This theorem is referenced by:  ad5ant124  1359  ixxin  12748  odf1  18611  m2cpmfo  21280  cnflf  22526  cnfcf  22566  tmdmulg  22616  blin  22946  blsscls2  23029  metcn  23068  xrsxmet  23332  sqf11  25630  dimval  30887  dfgcd3  34474  lindsadd  34752  hspmbllem2  42771
  Copyright terms: Public domain W3C validator