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

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

Proof of Theorem ad4ant14
StepHypRef Expression
1 ad4ant14.1 . . . 4 ((𝜑𝜓) → 𝜒)
21ex 448 . . 3 (𝜑 → (𝜓𝜒))
322a1d 26 . 2 (𝜑 → (𝜃 → (𝜏 → (𝜓𝜒))))
43imp41 616 1 ((((𝜑𝜃) ∧ 𝜏) ∧ 𝜓) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 195  df-an 384
This theorem is referenced by:  pntlem3  25010  hlpasch  25361  matunitlindflem1  32373  matunitlindflem2  32374  poimirlem26  32403  mblfinlem2  32415  ssfiunibd  38262  xralrple2  38310  infleinf  38328  fprodcn  38466  icccncfext  38572  cncficcgt0  38573  cncfioobd  38582  dvbdfbdioolem2  38618  itgspltprt  38670  stoweidlem34  38726  stoweidlem49  38741  stoweidlem57  38749  fourierdlem34  38833  fourierdlem39  38838  fourierdlem50  38848  fourierdlem51  38849  fourierdlem64  38862  fourierdlem73  38871  fourierdlem77  38875  fourierdlem81  38879  fourierdlem94  38892  fourierdlem97  38895  fourierdlem103  38901  fourierdlem104  38902  fourierdlem113  38911  fourier2  38919  etransclem24  38950  intsal  39023  sge0pr  39086  sge0iunmptlemfi  39105  sge0seq  39138  sge0reuz  39139  nnfoctbdjlem  39147  meadjiunlem  39157  ismeannd  39159  carageniuncllem2  39211  isomennd  39220  hoicvr  39237  hspmbllem2  39316  iunhoiioolem  39365  iunhoiioo  39366  vonioo  39372  vonicc  39375  preimageiingt  39406  preimaleiinlt  39407  smfaddlem1  39448  smfaddlem2  39449  smflimlem4  39459  smfrec  39473  lighneallem3  39862  lfgrwlkprop  40893  1wlkiswwlks1  41061  frgrnbnb  41460  frgrwopreglem5  41482
  Copyright terms: Public domain W3C validator