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 399
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 210  df-an 400
This theorem is referenced by:  ad5ant15  758  ad5ant25  761  soisoi  7064  dfac9  9551  lediv12a  11526  leexp1a  13539  seqcoll  13822  lo1bdd2  14877  rlimcld2  14931  rlimcn1  14941  isercolllem1  15017  summo  15070  climcnds  15202  geomulcvg  15228  mertenslem2  15237  prodmolem2  15285  prodmo  15286  fprod2d  15331  pwsle  16761  isacs2  16920  grprinvlem  17879  gsumpropd2lem  17885  gsumwsubmcl  17997  gsumwmhm  18006  mulgfval  18222  gaid  18425  gsmsymgrfixlem1  18551  mulgnn0di  18943  gsumval3  19024  fvmptnn04if  21458  cnpnei  21873  lfinun  22134  xkopt  22264  isr0  22346  fbflim  22585  alexsubALTlem3  22658  metss  23119  iscmet3lem2  23900  ovoliunlem3  24112  mbfposr  24260  i1fmulclem  24310  itg10a  24318  iblss  24412  dvlip  24600  plyeq0lem  24811  mtest  25003  itgulm  25007  dchrisumlem3  26079  rpvmasum2  26100  pntlem3  26197  hlpasch  26554  f1otrg  26669  lfgrwlkprop  27481  wlkiswwlks1  27657  frgrnbnb  28082  frgr2wwlkeqm  28120  unidifsnne  30312  hashxpe  30559  ccatf1  30655  signstfvneq0  31956  bnj605  32293  matunitlindflem1  35052  matunitlindflem2  35053  poimirlem26  35082  mblfinlem2  35094  ssfiunibd  41938  xralrple2  41983  infleinf  42001  infxrpnf  42081  fprodcn  42239  limsupub  42343  limsuppnflem  42349  limsupmnflem  42359  cnrefiisplem  42468  climxlim2lem  42484  icccncfext  42526  cncficcgt0  42527  cncfioobd  42536  dvbdfbdioolem2  42568  itgspltprt  42618  stoweidlem34  42673  stoweidlem49  42688  stoweidlem57  42696  fourierdlem34  42780  fourierdlem39  42785  fourierdlem50  42795  fourierdlem51  42796  fourierdlem64  42809  fourierdlem73  42818  fourierdlem77  42822  fourierdlem81  42826  fourierdlem94  42839  fourierdlem97  42842  fourierdlem103  42848  fourierdlem104  42849  fourierdlem113  42858  fourier2  42866  etransclem24  42897  intsal  42967  sge0pr  43030  sge0iunmptlemfi  43049  sge0seq  43082  sge0reuz  43083  nnfoctbdjlem  43091  meadjiunlem  43101  ismeannd  43103  carageniuncllem2  43158  isomennd  43167  hoicvr  43184  hspmbllem2  43263  iunhoiioolem  43311  iunhoiioo  43312  vonioo  43318  vonicc  43321  preimageiingt  43352  preimaleiinlt  43353  smfaddlem1  43393  smfaddlem2  43394  smflimlem4  43404  smfrec  43418  smfinflem  43445  sprsymrelf1lem  44005  lighneallem3  44122  isomgreqve  44340  1arymaptfo  45054
  Copyright terms: Public domain W3C validator