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 481 . 2 (((𝜑𝜓) ∧ 𝜏) → 𝜒)
32adantlll 714 1 ((((𝜃𝜑) ∧ 𝜓) ∧ 𝜏) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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
This theorem is referenced by:  fntpb  6963  suppssfv  7855  omsmolem  8269  ttukeylem5  9923  rlim3  14843  mp2pm2mplem4  21345  chfacfisf  21390  chfacfisfcpmat  21391  mbfi1fseqlem3  24245  usgredg2vlem2  26935  umgr3v3e3cycl  27890  matunitlindflem1  34769  matunitlindflem2  34770  heicant  34808  difmap  41346  xlimmnfvlem2  41990  xlimpnfvlem2  41994  xlimliminflimsup  42019  sge0resplit  42565  hoidmvle  42759  eenglngeehlnmlem2  44653
  Copyright terms: Public domain W3C validator