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

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

Proof of Theorem ad4ant13
StepHypRef Expression
1 ad4ant2.1 . . 3 ((𝜑𝜓) → 𝜒)
21adantlr 753 . 2 (((𝜑𝜃) ∧ 𝜓) → 𝜒)
32adantr 472 1 ((((𝜑𝜃) ∧ 𝜓) ∧ 𝜏) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 197  df-an 385
This theorem is referenced by:  ad5ant14  1218  ad5ant24  1224  fntpb  6638  dvdslcmf  15566  poslubmo  17367  posglbmo  17368  trust  22254  metust  22584  umgrres1lem  26422  upgrres1  26425  friendshipgt3  27587  repr0  31019  breprexplemc  31040  hgt750lemb  31064  matunitlindflem1  33736  mapss2  39914  supxrge  40070  xrlexaddrp  40084  infxr  40099  infleinf  40104  unb2ltle  40158  supminfxr  40210  limsuppnfdlem  40454  limsupub  40457  limsuppnflem  40463  climinf3  40469  limsupmnflem  40473  climxrre  40503  liminfvalxr  40536  sge0isum  41165  sge0gtfsumgt  41181  sge0seq  41184  nnfoctbdjlem  41193  meaiuninc3v  41222  omeiunltfirp  41257  hspdifhsp  41354  hspmbllem2  41365  pimdecfgtioo  41451  pimincfltioo  41452  preimageiingt  41454  preimaleiinlt  41455  smfid  41485  proththd  42059
  Copyright terms: Public domain W3C validator