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

Theorem ad4ant14 751
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 714 . 2 (((𝜑𝜃) ∧ 𝜓) → 𝜒)
32adantlr 714 1 ((((𝜑𝜃) ∧ 𝜏) ∧ 𝜓) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397
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 398
This theorem is referenced by:  ad5ant15  758  ad5ant25  761  soisoi  7278  dfac9  10079  lediv12a  12055  leexp1a  14087  seqcoll  14370  lo1bdd2  15413  rlimcld2  15467  rlimcn1  15477  isercolllem1  15556  summo  15609  climcnds  15743  geomulcvg  15768  mertenslem2  15777  prodmolem2  15825  prodmo  15826  fprod2d  15871  pwsle  17381  isacs2  17540  grprinvlem  18535  gsumpropd2lem  18541  gsumwsubmcl  18654  gsumwmhm  18662  mulgfval  18881  gaid  19086  gsmsymgrfixlem1  19216  mulgnn0di  19611  gsumval3  19691  fvmptnn04if  22214  cnpnei  22631  lfinun  22892  xkopt  23022  isr0  23104  fbflim  23343  alexsubALTlem3  23416  metss  23880  iscmet3lem2  24672  ovoliunlem3  24884  mbfposr  25032  i1fmulclem  25083  itg10a  25091  iblss  25185  dvlip  25373  plyeq0lem  25587  mtest  25779  itgulm  25783  dchrisumlem3  26855  rpvmasum2  26876  pntlem3  26973  nosupbday  27069  noinfbday  27084  hlpasch  27740  f1otrg  27855  lfgrwlkprop  28677  wlkiswwlks1  28854  frgrnbnb  29279  frgr2wwlkeqm  29317  unidifsnne  31505  hashxpe  31751  ccatf1  31847  signstfvneq0  33224  bnj605  33559  matunitlindflem1  36103  matunitlindflem2  36104  poimirlem26  36133  mblfinlem2  36145  ssfiunibd  43617  xralrple2  43662  infleinf  43680  infxrpnf  43755  fprodcn  43915  limsupub  44019  limsuppnflem  44025  limsupmnflem  44035  cnrefiisplem  44144  climxlim2lem  44160  icccncfext  44202  cncficcgt0  44203  cncfioobd  44212  dvbdfbdioolem2  44244  itgspltprt  44294  stoweidlem34  44349  stoweidlem49  44364  stoweidlem57  44372  fourierdlem34  44456  fourierdlem39  44461  fourierdlem50  44471  fourierdlem51  44472  fourierdlem64  44485  fourierdlem73  44494  fourierdlem77  44498  fourierdlem81  44502  fourierdlem94  44515  fourierdlem97  44518  fourierdlem103  44524  fourierdlem104  44525  fourierdlem113  44534  fourier2  44542  etransclem24  44573  intsal  44645  sge0pr  44709  sge0iunmptlemfi  44728  sge0seq  44761  sge0reuz  44762  nnfoctbdjlem  44770  meadjiunlem  44780  ismeannd  44782  carageniuncllem2  44837  isomennd  44846  hoicvr  44863  hspmbllem2  44942  iunhoiioolem  44990  iunhoiioo  44991  vonioo  44997  vonicc  45000  preimageiingt  45035  preimaleiinlt  45036  smfaddlem1  45078  smfaddlem2  45079  smflimlem4  45089  smfrec  45104  smfinflem  45132  sprsymrelf1lem  45757  lighneallem3  45873  isomgreqve  46091  1arymaptfo  46803
  Copyright terms: Public domain W3C validator