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

Theorem ad4ant13 751
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 ((𝜑𝜓) → 𝜒)
21adantr 480 . 2 (((𝜑𝜓) ∧ 𝜏) → 𝜒)
32adantllr 719 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:  ad5ant14  757  ad5ant24  760  fntpb  7230  peano5  7916  f1o2ndf1  8148  cantnfle  9712  cantnflem1c  9728  ttukeylem5  10554  rlimsqzlem  15686  dvdslcmf  16669  poslubmo  18457  posglbmo  18458  smndex1mgm  18921  isgrpinv  19012  ghmgrp  19085  dprdfcntz  20036  pzriprnglem4  21496  sraassab  21889  cply1coe0bi  22307  evls1fpws  22374  isnrm3  23368  cnextcn  24076  ustexsym  24225  ustex2sym  24226  ustex3sym  24227  trust  24239  fmucnd  24302  trcfilu  24304  metust  24572  cxpmul2z  26734  umgrres1lem  29328  upgrres1  29331  friendshipgt3  30418  ccatf1  32934  cyc3evpm  33171  elrgspnlem1  33247  elrgspnlem2  33248  elrgspnlem4  33250  elrgspnsubrunlem1  33252  elrgspnsubrunlem2  33253  znfermltl  33395  rhmimaidl  33461  dimlssid  33684  txomap  33834  zart0  33879  repr0  34627  breprexplemc  34648  hgt750lemb  34672  satffunlem1lem2  35409  satffunlem2lem2  35412  lindsadd  37621  matunitlindflem1  37624  nadd1suc  43410  mapss2  45215  supxrge  45354  xrlexaddrp  45368  infxr  45383  infleinf  45388  unb2ltle  45431  supminfxr  45480  limsuppnfdlem  45721  limsupub  45724  limsuppnflem  45730  climinf3  45736  limsupmnflem  45740  climxrre  45770  liminfvalxr  45803  fperdvper  45939  sge0isum  46447  sge0gtfsumgt  46463  sge0seq  46466  nnfoctbdjlem  46475  meaiuninc3v  46504  omeiunltfirp  46539  hspdifhsp  46636  hspmbllem2  46647  pimdecfgtioo  46737  pimincfltioo  46738  preimageiingt  46740  preimaleiinlt  46741  smfid  46772  proththd  47606
  Copyright terms: Public domain W3C validator