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

Theorem ad4ant134 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
ad4ant134 ((((𝜑𝜏) ∧ 𝜓) ∧ 𝜒) → 𝜃)

Proof of Theorem ad4ant134
StepHypRef Expression
1 ad4ant3.1 . . 3 ((𝜑𝜓𝜒) → 𝜃)
213expa 1117 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
32adantllr 719 1 ((((𝜑𝜏) ∧ 𝜓) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1086
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 207  df-an 396  df-3an 1088
This theorem is referenced by:  ad5ant245  1360  ad5ant134  1366  ad5ant135  1367  ad5ant145  1368  ralxfrd2  5418  gruwun  10851  lemul12b  12122  initoeu1  18065  termoeu1  18072  quscrng  21311  metss  24537  wlkswwlksf1o  29909  climxlim2lem  45801  smflimlem4  46730  isubgr3stgrlem8  47876
  Copyright terms: Public domain W3C validator