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

Theorem ad4ant14 750
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
ad4ant14 ((((𝜑𝜃) ∧ 𝜏) ∧ 𝜓) → 𝜒)

Proof of Theorem ad4ant14
StepHypRef Expression
1 ad4ant2.1 . . 3 ((𝜑𝜓) → 𝜒)
21adantlr 713 . 2 (((𝜑𝜃) ∧ 𝜓) → 𝜒)
32adantlr 713 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 206  df-an 397
This theorem is referenced by:  ad5ant15  757  ad5ant25  760  soisoi  7272  dfac9  10071  lediv12a  12047  leexp1a  14079  seqcoll  14362  lo1bdd2  15405  rlimcld2  15459  rlimcn1  15469  isercolllem1  15548  summo  15601  climcnds  15735  geomulcvg  15760  mertenslem2  15769  prodmolem2  15817  prodmo  15818  fprod2d  15863  pwsle  17373  isacs2  17532  grprinvlem  18527  gsumpropd2lem  18533  gsumwsubmcl  18646  gsumwmhm  18654  mulgfval  18872  gaid  19077  gsmsymgrfixlem1  19207  mulgnn0di  19602  gsumval3  19682  fvmptnn04if  22196  cnpnei  22613  lfinun  22874  xkopt  23004  isr0  23086  fbflim  23325  alexsubALTlem3  23398  metss  23862  iscmet3lem2  24654  ovoliunlem3  24866  mbfposr  25014  i1fmulclem  25065  itg10a  25073  iblss  25167  dvlip  25355  plyeq0lem  25569  mtest  25761  itgulm  25765  dchrisumlem3  26837  rpvmasum2  26858  pntlem3  26955  nosupbday  27051  noinfbday  27066  hlpasch  27696  f1otrg  27811  lfgrwlkprop  28633  wlkiswwlks1  28810  frgrnbnb  29235  frgr2wwlkeqm  29273  unidifsnne  31461  hashxpe  31704  ccatf1  31800  signstfvneq0  33175  bnj605  33510  matunitlindflem1  36065  matunitlindflem2  36066  poimirlem26  36095  mblfinlem2  36107  ssfiunibd  43519  xralrple2  43564  infleinf  43582  infxrpnf  43657  fprodcn  43813  limsupub  43917  limsuppnflem  43923  limsupmnflem  43933  cnrefiisplem  44042  climxlim2lem  44058  icccncfext  44100  cncficcgt0  44101  cncfioobd  44110  dvbdfbdioolem2  44142  itgspltprt  44192  stoweidlem34  44247  stoweidlem49  44262  stoweidlem57  44270  fourierdlem34  44354  fourierdlem39  44359  fourierdlem50  44369  fourierdlem51  44370  fourierdlem64  44383  fourierdlem73  44392  fourierdlem77  44396  fourierdlem81  44400  fourierdlem94  44413  fourierdlem97  44416  fourierdlem103  44422  fourierdlem104  44423  fourierdlem113  44432  fourier2  44440  etransclem24  44471  intsal  44543  sge0pr  44607  sge0iunmptlemfi  44626  sge0seq  44659  sge0reuz  44660  nnfoctbdjlem  44668  meadjiunlem  44678  ismeannd  44680  carageniuncllem2  44735  isomennd  44744  hoicvr  44761  hspmbllem2  44840  iunhoiioolem  44888  iunhoiioo  44889  vonioo  44895  vonicc  44898  preimageiingt  44933  preimaleiinlt  44934  smfaddlem1  44976  smfaddlem2  44977  smflimlem4  44987  smfrec  45002  smfinflem  45030  sprsymrelf1lem  45655  lighneallem3  45771  isomgreqve  45989  1arymaptfo  46701
  Copyright terms: Public domain W3C validator