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

Theorem ad4ant13 758
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 707 . 2 (((𝜑𝜃) ∧ 𝜓) → 𝜒)
32adantr 473 1 ((((𝜑𝜃) ∧ 𝜓) ∧ 𝜏) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 385
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 199  df-an 386
This theorem is referenced by:  ad5ant14  770  ad5ant24  776  fntpb  6701  dvdslcmf  15676  poslubmo  17458  posglbmo  17459  trust  22358  metust  22688  umgrres1lem  26537  upgrres1  26540  friendshipgt3  27776  repr0  31202  breprexplemc  31223  hgt750lemb  31247  matunitlindflem1  33887  mapss2  40138  supxrge  40287  xrlexaddrp  40301  infxr  40316  infleinf  40321  unb2ltle  40374  supminfxr  40426  limsuppnfdlem  40666  limsupub  40669  limsuppnflem  40675  climinf3  40681  limsupmnflem  40685  climxrre  40715  liminfvalxr  40748  fperdvper  40866  sge0isum  41376  sge0gtfsumgt  41392  sge0seq  41395  nnfoctbdjlem  41404  meaiuninc3v  41433  omeiunltfirp  41468  hspdifhsp  41565  hspmbllem2  41576  pimdecfgtioo  41662  pimincfltioo  41663  preimageiingt  41665  preimaleiinlt  41666  smfid  41696  proththd  42302
  Copyright terms: Public domain W3C validator