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

Theorem ad4ant13 1284
Description: Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.)
Hypothesis
Ref Expression
ad4ant13.1 ((𝜑𝜓) → 𝜒)
Assertion
Ref Expression
ad4ant13 ((((𝜑𝜃) ∧ 𝜓) ∧ 𝜏) → 𝜒)

Proof of Theorem ad4ant13
StepHypRef Expression
1 ad4ant13.1 . . . . 5 ((𝜑𝜓) → 𝜒)
21ex 449 . . . 4 (𝜑 → (𝜓𝜒))
32a1dd 48 . . 3 (𝜑 → (𝜓 → (𝜏𝜒)))
43a1d 25 . 2 (𝜑 → (𝜃 → (𝜓 → (𝜏𝜒))))
54imp41 617 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 196  df-an 385
This theorem is referenced by:  fntpb  6378  dvdslcmf  15182  trust  21843  metust  22173  matunitlindflem1  32575  mapss2  38392  supxrge  38495  xrlexaddrp  38509  infxr  38524  infleinf  38529  sge0isum  39320  sge0gtfsumgt  39336  sge0seq  39339  nnfoctbdjlem  39348  omeiunltfirp  39409  hspdifhsp  39506  hspmbllem2  39517  pimdecfgtioo  39604  pimincfltioo  39605  preimageiingt  39607  preimaleiinlt  39608  smfid  39639  proththd  40069  umgrres1lem  40529  upgrres1  40532  av-friendshipgt3  41552
  Copyright terms: Public domain W3C validator