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

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

Proof of Theorem ad4ant24
StepHypRef Expression
1 ad4ant2.1 . . 3 ((𝜑𝜓) → 𝜒)
21adantlr 711 . 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:  oaass  8176  oewordri  8207  infxp  9625  lediv12a  11521  xmulgt0  12664  ioodisj  12856  leexp1a  13527  swrdswrdlem  14054  seqshft  14432  sumss2  15071  mulgfval  18164  grpissubg  18237  f1otrspeq  18504  mat1dimcrng  21014  elcls  21609  neiptopreu  21669  alexsubALTlem4  22586  ustuqtop2  22778  iscfil2  23796  tglowdim1i  26214  axcontlem2  26678  opreu2reuALT  30167  matunitlindflem1  34769  matunitlindflem2  34770  founiiun0  41327  xralrple2  41498  rexabslelem  41568  climisp  41903  climxrre  41907  cnrefiisplem  41986  sge0iunmptlemre  42574  nnfoctbdjlem  42614  iundjiun  42619  meaiuninc3v  42643  hoidmvlelem3  42756  hspmbllem2  42786  smflimlem2  42925
  Copyright terms: Public domain W3C validator