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

Theorem ad4ant24 754
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 715 . 2 (((𝜑𝜏) ∧ 𝜓) → 𝜒)
32adantlll 718 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 207  df-an 396
This theorem is referenced by:  oaass  8600  oewordri  8631  naddssim  8724  infxp  10255  lediv12a  12162  xmulgt0  13326  ioodisj  13523  leexp1a  14216  swrdswrdlem  14743  seqshft  15125  sumss2  15763  prmdvdsncoprmbd  16765  mulgfval  19088  grpissubg  19165  f1otrspeq  19466  mat1dimcrng  22484  elcls  23082  neiptopreu  23142  alexsubALTlem4  24059  ustuqtop2  24252  iscfil2  25301  absmuls  28269  tglowdim1i  28510  axcontlem2  28981  opreu2reuALT  32497  nsgqusf1olem1  33442  lbslelsp  33649  matunitlindflem1  37624  matunitlindflem2  37625  poimirlem4  37632  founiiun0  45200  xralrple2  45370  rexabslelem  45434  climisp  45766  climxrre  45770  cnrefiisplem  45849  sge0iunmptlemre  46435  nnfoctbdjlem  46475  iundjiun  46480  meaiuninc3v  46504  hoidmvlelem3  46617  hspmbllem2  46647  smflimlem2  46792
  Copyright terms: Public domain W3C validator