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

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

Proof of Theorem ad5ant15
StepHypRef Expression
1 ad5ant2.1 . . 3 ((𝜑𝜓) → 𝜒)
21adantlr 711 . 2 (((𝜑𝜃) ∧ 𝜓) → 𝜒)
32ad4ant14 748 1 (((((𝜑𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜓) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394
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 395
This theorem is referenced by:  summolem2  15666  ntrivcvg  15847  xkoccn  23343  abelthlem8  26187  rpvmasum2  27251  mulog2sumlem2  27274  f1otrge  28390  nn0xmulclb  32251  intlidl  32810  ply1degltdimlem  32995  fedgmul  33004  signstfvneq0  33881  breprexplemc  33942  mblfinlem2  36829  supxrgelem  44345  supxrge  44346  rexabslelem  44426  uzub  44439  smflimlem4  45788
  Copyright terms: Public domain W3C validator