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

Theorem ad4ant23 749
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 479 . 2 (((𝜑𝜓) ∧ 𝜏) → 𝜒)
32adantlll 714 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:  fntpb  7212  suppssfv  8189  omsmolem  8658  ttukeylem5  10510  rlim3  15446  mp2pm2mplem4  22531  chfacfisf  22576  chfacfisfcpmat  22577  mbfi1fseqlem3  25467  usgredg2vlem2  28750  umgr3v3e3cycl  29704  matunitlindflem1  36787  matunitlindflem2  36788  heicant  36826  naddgeoa  42447  difmap  44204  xlimmnfvlem2  44847  xlimpnfvlem2  44851  xlimliminflimsup  44876  sge0resplit  45420  hoidmvle  45614  eenglngeehlnmlem2  47511
  Copyright terms: Public domain W3C validator