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

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

Proof of Theorem ad4ant23
StepHypRef Expression
1 ad4ant2.1 . . 3 ((𝜑𝜓) → 𝜒)
21adantr 480 . 2 (((𝜑𝜓) ∧ 𝜏) → 𝜒)
32adantlll 715 1 ((((𝜃𝜑) ∧ 𝜓) ∧ 𝜏) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395
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 396
This theorem is referenced by:  fntpb  7213  suppssfv  8190  omsmolem  8659  ttukeylem5  10511  rlim3  15447  mp2pm2mplem4  22532  chfacfisf  22577  chfacfisfcpmat  22578  mbfi1fseqlem3  25468  usgredg2vlem2  28751  umgr3v3e3cycl  29705  matunitlindflem1  36788  matunitlindflem2  36789  heicant  36827  naddgeoa  42448  difmap  44205  xlimmnfvlem2  44848  xlimpnfvlem2  44852  xlimliminflimsup  44877  sge0resplit  45421  hoidmvle  45615  eenglngeehlnmlem2  47512
  Copyright terms: Public domain W3C validator