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

Theorem ad4ant13 747
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 481 . 2 (((𝜑𝜓) ∧ 𝜏) → 𝜒)
32adantllr 715 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:  ad5ant14  754  ad5ant24  757  fntpb  6838  peano5  7461  f1o2ndf1  7671  cantnfle  8980  cantnflem1c  8996  ttukeylem5  9781  rlimsqzlem  14839  dvdslcmf  15804  poslubmo  17585  posglbmo  17586  isgrpinv  17913  ghmgrp  17980  dprdfcntz  18854  cply1coe0bi  20151  isnrm3  21651  cnextcn  22359  ustexsym  22507  ustex2sym  22508  ustex3sym  22509  trust  22521  fmucnd  22584  trcfilu  22586  metust  22851  cxpmul2z  24955  umgrres1lem  26775  upgrres1  26778  friendshipgt3  27869  cyc3evpm  30430  repr0  31499  breprexplemc  31520  hgt750lemb  31544  satffunlem1lem2  32258  satffunlem2lem2  32261  lindsadd  34416  matunitlindflem1  34419  mapss2  41008  supxrge  41147  xrlexaddrp  41161  infxr  41176  infleinf  41181  unb2ltle  41231  supminfxr  41282  limsuppnfdlem  41524  limsupub  41527  limsuppnflem  41533  climinf3  41539  limsupmnflem  41543  climxrre  41573  liminfvalxr  41606  fperdvper  41744  sge0isum  42251  sge0gtfsumgt  42267  sge0seq  42270  nnfoctbdjlem  42279  meaiuninc3v  42308  omeiunltfirp  42343  hspdifhsp  42440  hspmbllem2  42451  pimdecfgtioo  42537  pimincfltioo  42538  preimageiingt  42540  preimaleiinlt  42541  smfid  42571  proththd  43261
  Copyright terms: Public domain W3C validator