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

Theorem 3ad2ant3 1082
Description: Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)
Hypothesis
Ref Expression
3ad2ant.1 (𝜑𝜒)
Assertion
Ref Expression
3ad2ant3 ((𝜓𝜃𝜑) → 𝜒)

Proof of Theorem 3ad2ant3
StepHypRef Expression
1 3ad2ant.1 . . 3 (𝜑𝜒)
21adantl 482 . 2 ((𝜃𝜑) → 𝜒)
323adant1 1077 1 ((𝜓𝜃𝜑) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1036
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 197  df-an 386  df-3an 1038
This theorem is referenced by:  simp3l  1087  simp3r  1088  simp31  1095  simp32  1096  simp33  1097  simp3ll  1130  simp3lr  1131  simp3rl  1132  simp3rr  1133  simp3l1  1164  simp3l2  1165  simp3l3  1166  simp3r1  1167  simp3r2  1168  simp3r3  1169  simp31l  1182  simp31r  1183  simp32l  1184  simp32r  1185  simp33l  1186  simp33r  1187  simp311  1206  simp312  1207  simp313  1208  simp321  1209  simp322  1210  simp323  1211  simp331  1212  simp332  1213  simp333  1214  3anim123i  1245  3jaao  1394  ceqsalt  3223  ceqsralt  3224  vtoclgftOLD  3250  disjtpsn  4242  disjtp2  4243  elpwdifsn  4310  ssprsseq  4348  tpssi  4360  prnebg  4380  poltletr  5516  predeq123  5669  predpo  5686  funprgOLD  5929  funtpgOLD  5931  fntpg  5936  funcnvpr  5938  funcnvtp  5939  ftpg  6408  fsnunf  6436  fsnunfv  6438  fvpr1g  6443  fvpr2g  6444  fpropnf1  6509  weniso  6589  ovmpt3rab1  6876  epne3  6965  limsuc  7034  oteqimp  7172  el2xptp0  7197  funsssuppss  7306  smoel  7442  smoord  7447  omwordi  7636  oneo  7646  oeord  7653  oewordi  7656  nnmwordi  7700  nnneo  7716  uniinqs  7812  undifixp  7929  enfixsn  8054  domss2  8104  domssex2  8105  unxpdomlem3  8151  dif1en  8178  rneqdmfinf1o  8227  mapfien2  8299  dffi2  8314  unwdomg  8474  ixpiunwdom  8481  en3lplem1  8496  oemapvali  8566  fodomfi2  8868  infcdaabs  9013  infunabs  9014  infdif  9016  ackbij1lem9  9035  ackbij1lem16  9042  coflim  9068  cfsmolem  9077  isfin2-2  9126  fin1a2lem9  9215  hsmexlem2  9234  axcc2lem  9243  axcc3  9245  domtriomlem  9249  axdc3lem4  9260  axcclem  9264  zornn0g  9312  axacndlem4  9417  axacndlem5  9418  axacnd  9419  gchdomtri  9436  fpwwe  9453  tskssel  9564  tskint  9592  tskurn  9596  gruurn  9605  gruixp  9616  grudomon  9624  gruina  9625  adderpqlem  9761  mulerpqlem  9762  addassnq  9765  mulassnq  9766  distrnq  9768  ltsonq  9776  ltanq  9778  ltmnq  9779  reclem3pr  9856  dedekind  10185  addid2  10204  addcan2  10206  divdir  10695  divcan5  10712  ltdiv1  10872  infrelb  10993  lt2halves  11252  zdivmul  11434  ledivge1le  11886  addlelt  11927  xaddass  12064  xleadd1  12070  xltadd1  12071  xmulasslem3  12101  xmulass  12102  xlemul1  12105  xlemul2  12106  xltmul1  12107  xadddir  12111  elioo5  12216  iccsupr  12251  iccneg  12278  icoshft  12279  icoshftf1o  12280  iccsplit  12290  zltaddlt1le  12309  fzen  12343  ssfzunsn  12372  elfz1b  12394  fzrevral  12409  fzshftral  12412  elfz0ubfz0  12427  elfz0fzfz0  12428  fz0fzelfz0  12429  fz0fzdiffz0  12432  elfzo  12456  elfzonlteqm1  12527  ltdifltdiv  12618  modabs  12686  modcyc  12688  modaddmulmod  12720  moddi  12721  modsubdir  12722  expdiv  12894  leexp2a  12899  bcval3  13076  hashnnn0genn0  13114  hashgadd  13149  hashunx  13158  hashfun  13207  hashres  13208  hash2prd  13240  hashtpg  13250  fun2dmnop0  13259  brfi1indlem  13261  ccatval1  13344  ccatval2  13345  ccatval3  13346  ccatsymb  13349  ccatass  13354  ccats1val2  13386  swrdval2  13402  swrd0len0  13418  swrd0fv  13421  swrdeq  13426  swrdspsleq  13431  2swrdeqwrdeq  13435  swrdswrdlem  13441  swrdswrd  13442  swrd0swrd  13443  ccats1swrdeq  13451  ccats1swrdeqrex  13460  swrdccatin12lem2  13470  swrdccat3b  13477  swrdccatid  13478  splval  13483  repswswrd  13512  cshwidxmod  13530  cshwidx0mod  13532  cshf1  13537  cshwleneq  13544  scshwfzeqfzo  13553  cshimadifsn  13556  cshimadifsn0  13557  ccatco  13562  cshco  13563  swrdco  13564  f1oun2prg  13643  swrds2  13666  eqwrds3  13685  trclfvss  13728  elicc4abs  14040  mulcn2  14307  fsumsplitsnun  14465  fsumsplitsnunOLD  14467  modfsummods  14506  prodfrec  14608  ntrivcvgfvn0  14612  binomrisefac  14754  demoivreALT  14912  rpnnen2lem4  14927  dvdsval2  14967  modmulconst  14994  dvdsexp  15030  oddge22np1  15054  modremain  15113  mulgcd  15246  mulgcdr  15248  gcddiv  15249  rpmulgcd  15256  rplpwr  15257  lcmfn0val  15317  lcmftp  15330  lcmfunsnlem2lem1  15332  lcmfunsnlem2lem2  15333  lcmfunsnlem2  15334  coprmdvds  15347  cncongr1  15362  dvdsnprmd  15384  prmexpb  15411  rpexp  15413  cncongrprm  15418  modprm0  15491  modprmn0modprm0  15493  coprimeprodsq  15494  pythagtriplem1  15502  pythagtriplem3  15504  pythagtriplem10  15506  pythagtriplem6  15507  pythagtriplem11  15511  pythagtriplem12  15512  pythagtriplem13  15513  pythagtriplem15  15515  pythagtriplem17  15517  pythagtriplem19  15519  pcdvdsb  15554  dvdsprmpweqle  15571  pcfaclem  15583  vdwapun  15659  ramval  15693  0ram2  15706  0ramcl  15708  fvprmselgcd1  15730  prmgaplem6  15741  setsstructOLD  15880  imasaddvallem  16170  imasvscaval  16179  mreiincl  16237  mremre  16245  mrieqv2d  16280  cofurid  16532  initoeu2lem0  16644  initoeu2lem2  16646  funcestrcsetclem6  16766  funcestrcsetclem9  16769  funcsetcestrclem6  16781  funcsetcestrclem9  16784  xpcpropd  16829  clatleglb  17107  ress0g  17300  gsumccat  17359  gsumccatsn  17361  sgrp2nmndlem3  17393  sgrp2nmndlem5  17397  dfgrp3lem  17494  mulgdirlem  17553  mulgp1  17555  mulgmodid  17562  eqglact  17626  fvcosymgeq  17830  gsmsymgreqlem2  17832  pmtrprfv3  17855  pmtr3ncomlem1  17874  mndodcongi  17943  oddvdsnn0  17944  odngen  17973  gexnnod  17984  lsmlub  18059  lsmass  18064  efgsval2  18127  efgsrel  18128  ghmplusg  18230  odadd1  18232  odadd2  18233  srg1zr  18510  dvrcan1  18672  dvrcan3  18673  irredrmul  18688  srngadd  18838  srngmul  18839  rmodislmodlem  18911  rmodislmod  18912  lmhmvsca  19026  reslmhm2  19034  pwssplit3  19042  lbspss  19063  lsmsp  19067  lspsneu  19104  lidldvgen  19236  assa2ass  19303  evlsval  19500  evlsval2  19501  psropprmul  19589  coe1add  19615  coe1addfv  19616  coe1subfv  19617  coe1tm  19624  coe1sclmul  19633  coe1sclmul2  19635  coe1fzgsumdlem  19652  lply1binom  19657  evl1gsumdlem  19701  zrhpsgninv  19912  zrhpsgnevpm  19918  zrhpsgnodpm  19919  psgndiflemB  19927  cssmre  20018  frlmup4  20121  islindf2  20134  lindsind2  20139  f1lindf  20142  lindsss  20144  f1linds  20145  lindsmm  20148  lbslcic  20161  mndvcl  20178  mndvass  20179  mhmvlin  20184  matecl  20212  matvscacell  20223  mamulid  20228  mamurid  20229  mattposm  20246  madetsumid  20248  matepmcl  20249  matepm2cl  20250  mat1dimbas  20259  mavmulsolcl  20338  mulmarep1el  20359  mulmarep1gsum1  20360  mulmarep1gsum2  20361  1marepvsma1  20370  m1detdiag  20384  mdetdiaglem  20385  mdetdiag  20386  mdetunilem7  20405  mdetunilem9  20407  mdetmul  20410  gsummatr01lem3  20444  gsummatr01lem4  20445  gsummatr01  20446  smadiadetglem2  20459  matinv  20464  slesolinv  20467  cramerimplem1  20470  cramerimp  20473  cramerlem1  20474  pmatcoe1fsupp  20487  mat2pmatbas  20512  decpmatmullem  20557  pmatcollpw3lem  20569  chpscmat  20628  iuncld  20830  clsss  20839  ntrcls0  20861  iscldtop  20880  neiss  20894  neips  20898  restcldi  20958  cnpnei  21049  cnconst2  21068  cnpresti  21073  sslm  21084  cnt0  21131  cnt1  21135  cnhaus  21139  cncmp  21176  cmpcld  21186  cnconn  21206  conncompss  21217  ssref  21296  elptr  21357  upxp  21407  qtoptop2  21483  ordthmeolem  21585  opnfbas  21627  isfil2  21641  fbasweak  21650  snfbas  21651  fgss  21658  fgcl  21663  fbasrn  21669  trnei  21677  cfinfil  21678  csdfil  21679  supfil  21680  filufint  21705  fin1aufil  21717  fmval  21728  fmf  21730  elfm  21732  elfm3  21735  imaelfm  21736  rnelfmlem  21737  rnelfm  21738  flimclslem  21769  flfneii  21777  cnpfcfi  21825  alexsubALT  21836  ptcmplem3  21839  ustref  22003  ustelimasn  22007  utop3cls  22036  ressusp  22050  cfiluexsm  22075  prdsxmetlem  22154  txmetcn  22334  nmmtri  22407  nmrtri  22409  unitnmn0  22453  nminvr  22454  nmotri  22524  nghmplusg  22525  isclmi  22858  isclmp  22878  ncvsi  22932  fmcfil  23051  srabn  23137  rrxmvallem  23168  itgconst  23566  dvn2bss  23674  deg1mul3  23856  deg1mul3le  23857  deg1tmle  23858  q1peqb  23895  r1pcl  23898  r1pdeglt  23899  r1pid  23900  dvdsq1p  23901  dvdsr1p  23902  ptolemy  24229  sincosq1eq  24245  logeq0im1  24305  logmul2  24343  logdiv2  24344  cxplt2  24425  logbchbase  24490  relogbreexp  24494  relogbexp  24499  pythag  24528  lgamgulmlem1  24736  bcmono  24983  efexple  24987  lgsdirnn0  25050  gausslemma2dlem1a  25071  gausslemma2dlem3  25074  2lgslem1a1  25095  2lgsoddprmlem1  25114  2lgsoddprmlem2  25115  selberglem3  25217  brbtwn2  25766  axcgrid  25777  ax5seglem1  25789  ax5seglem2  25790  ax5seg  25799  axpasch  25802  axlowdimlem16  25818  axcontlem7  25831  structiedg0val  25892  lpvtx  25944  incistruhgr  25955  upgredg2vtx  26017  upgredgpr  26018  edglnl  26019  ausgrumgri  26043  ausgrusgri  26044  usgredg2vtxeuALT  26095  ushgredgedg  26102  ushgredgedgloop  26104  uspgr1v1eop  26122  usgr1v0edg  26130  uhgrissubgr  26148  egrsubgr  26150  0uhgrsubgr  26152  nbupgrres  26247  nb3grprlem1  26263  cplgr3v  26312  umgr2v2enb1  26403  finsumvtxdgeven  26429  vtxdgoddnumeven  26430  rusgrnumwrdl2  26463  rusgr1vtx  26465  isewlk  26479  ewlkinedg  26481  upgrewlkle2  26483  wlkvtxeledg  26500  wlkeq  26510  wlkl1loop  26515  wlk1walk  26516  uspgr2wlkeq  26523  uspgr2wlkeq2  26524  wlksoneq1eq2  26541  wlkonl1iedg  26542  wlkon2n0  26543  wlkres  26548  wlkp1lem8  26558  lfgriswlk  26566  lfgrwlknloop  26567  spthonpthon  26628  spthonepeq  26629  uhgrwkspth  26632  usgr2wlkspth  26636  usgr2pth  26641  wwlknp  26715  0enwwlksnge1  26730  wwlksnred  26768  wwlksnredwwlkn  26771  wwlksnextsur  26776  wlksnwwlknvbij  26784  umgr2adedgwlkonALT  26824  umgr2wlkon  26827  umgrwwlks2on  26831  elwspths2spth  26843  rusgr0edg  26849  rusgrnumwwlks  26850  clwwlksf  26895  clwwlksvbij  26902  clwwlksext2edg  26903  clwwisshclwwslemlem  26906  clwlksfclwwlk  26942  clwlksf1clwwlklem2  26946  clwlksf1clwwlklem  26948  clwwlksnun  26954  1ewlk  26956  1pthon2v  26993  3wlkdlem9  27008  uhgr3cyclex  27022  umgr3cyclex  27023  upgr4cycl4dv4e  27025  upgreupthseg  27049  eupth2lem3lem6  27073  eulercrct  27082  nfrgr2v  27116  frgr3vlem1  27117  3vfriswmgr  27122  extwwlkfablem1  27182  numclwwlkovf2ex  27191  extwwlkfab  27194  numclwlk1lem2foa  27195  numclwlk1lem2f1  27198  numclwlk1lem2fo  27199  numclwwlk1  27202  numclwwlk2lem1  27206  numclwlk2lem2f  27207  numclwlk2lem2f1o  27209  numclwwlk2  27211  numclwwlk3  27213  numclwwlk5lem  27215  numclwwlk6  27218  frgrreggt1  27221  frgrreg  27222  frgrregord013  27223  vcidOLD  27389  vcdi  27390  vcdir  27391  vcass  27392  imsmetlem  27515  0oval  27613  ajval  27687  shlub  28243  hmopco  28852  adjlnop  28915  mdslmd4i  29162  fcoinvbr  29391  fresf1o  29406  divnumden2  29538  ressnm  29625  ress1r  29763  smatfval  29835  pstmfval  29913  pl1cn  29975  ind1  30053  ind0  30054  sigaclcuni  30155  sigagenss2  30187  measun  30248  measvuni  30251  dya2iocnrect  30317  omsmeas  30359  ballotlemieq  30552  ballotlemrv1  30556  sgn3da  30577  bnj837  30805  bnj517  30929  bnj553  30942  bnj594  30956  bnj967  30989  bnj1097  31023  bnj1110  31024  bnj1118  31026  bnj1128  31032  bnj1125  31034  bnj1145  31035  bnj1136  31039  bnj1173  31044  bnj1189  31051  bnj1204  31054  bnj1279  31060  bnj1321  31069  bnj1413  31077  erdszelem2  31148  cnpconn  31186  cvmscld  31229  mrsubcv  31381  mrsubvr  31382  iprodefisumlem  31601  dvdspw  31611  dfon2lem3  31664  dfon2lem7  31668  frrlem4  31757  nosupfv  31826  nosupres  31827  noetalem1  31837  btwndiff  32109  brcolinear2  32140  btwnconn1  32183  nn0prpwlem  32292  hmeoclda  32303  hmeocldb  32304  ivthALT  32305  fnemeet1  32336  fnejoin1  32338  nnssi3  32430  nndivsub  32431  bj-ceqsalt1  32849  bj-evalidval  33006  onsucuni3  33186  curfv  33360  lindsdom  33374  lindsenlbs  33375  ftc1anclem4  33459  areacirclem2  33472  areacirclem5  33475  areacirc  33476  upixp  33495  filbcmb  33506  cnresima  33534  smprngopr  33822  igenval2  33836  lsmsat  34114  lsmsatcv  34116  lsatcvatlem  34155  islshpcv  34159  l1cvpat  34160  lfli  34167  lshpset2N  34225  cvrnbtwn  34377  meetat2  34403  atcmp  34417  atcvreq0  34420  atlatmstc  34425  cvlcvr1  34445  cvlcvrp  34446  cvlatcvr2  34448  cvr2N  34516  cvratlem  34526  2atjm  34550  athgt  34561  2lplnmN  34664  2llnmj  34665  2lplnmj  34727  dalemswapyzps  34795  dalem23  34801  dalem24  34802  dalem25  34803  dalem27  34804  dalem28  34805  dalem38  34815  dalem39  34816  dalem44  34821  dalem45  34822  dalem51  34828  dalem52  34829  dalem56  34833  pmapglbx  34874  pmapjat1  34958  pmapjat2  34959  paddatclN  35054  osumcllem4N  35064  osumcllem7N  35067  ltrncoval  35250  cdleme0aa  35316  cdleme0b  35318  cdleme8  35356  cdlemesner  35402  cdleme22eALTN  35452  cdleme26eALTN  35468  cdleme35h  35563  cdleme50trn2  35658  cdleme  35667  tgrpov  35855  tendotp  35868  tendoidcl  35876  tendo0co2  35895  cdlemkvcl  35949  dvhopvadd  36201  dvhopellsm  36225  dihmeetlem1N  36398  dihmeetlem9N  36423  dihatexv  36446  lcfl7lem  36607  mapdrvallem2  36753  mapdh9a  36898  hdmapevec  36946  ismrcd1  37080  istopclsd  37082  ismrc  37083  mapfzcons  37098  eldioph2  37144  diophrex  37158  diophren  37196  pellexlem1  37212  pellexlem5  37216  pellqrexplicit  37260  reglogmul  37276  reglogexp  37277  rmxycomplete  37301  congmul  37353  congabseq  37360  acongsym  37362  acongneg2  37363  fzneg  37368  acongeq  37369  jm2.19  37379  jm2.22  37381  jm2.23  37382  jm2.20nn  37383  rmydioph  37400  rmxdiophlem  37401  jm3.1  37406  pwssplit4  37478  hbtlem2  37513  idomrootle  37592  pwinfi2  37686  relexpaddss  37829  trclimalb2  37837  brtrclfv2  37838  trclfvdecomr  37839  ntrclsneine0lem  38182  ntrclsk2  38186  ntrclsk3  38188  ntrclsk13  38189  ntrclsk4  38190  gneispace  38252  dvconstbi  38353  expgrowth  38354  chordthmALT  38989  restuni3  39121  wessf1ornlem  39187  disjf1o  39194  elrnmpt2id  39243  funimassd  39247  infnsuprnmpt  39281  infrnmptle  39463  fmul01lt1lem1  39616  climsuselem1  39639  climsuse  39640  limcperiod  39660  lptre2pt  39672  climbddf  39719  limsupvaluz2  39770  supcnvlimsup  39772  cncfshift  39850  cncfperiod  39855  icccncfext  39863  dvnmptconst  39919  dvnprodlem1  39924  dvnprodlem2  39925  iblspltprt  39952  itgspltprt  39958  stoweidlem3  39983  stoweidlem16  39996  stoweidlem17  39997  stoweidlem26  40006  stoweidlem34  40014  stoweidlem57  40037  fourierdlem41  40128  fourierdlem42  40129  fourierdlem52  40138  fourierdlem54  40140  fourierdlem74  40160  fourierdlem75  40161  fourierdlem80  40166  fourierdlem94  40180  fourierdlem102  40188  fourierdlem114  40200  etransclem18  40232  etransclem29  40243  etransclem46  40260  rrxtopnfi  40269  subsaliuncl  40339  sge0f1o  40362  sge0xp  40409  meadjiunlem  40445  voliunsge0lem  40452  volmea  40454  carageniuncllem1  40498  caratheodorylem1  40503  caratheodory  40505  isomenndlem  40507  hoicvr  40525  ovnsubaddlem2  40548  hoidmvlelem1  40572  hoidmvlelem2  40573  hoidmvlelem3  40574  hspmbllem2  40604  smfaddlem1  40734  smfco  40772  smfsuplem1  40780  2leaddle2  41075  ssfz12  41087  fsumsplitsndif  41107  fsummmodsndifre  41108  fsummmodsnunz  41109  iccpartiltu  41122  icceuelpart  41136  pfxnd  41160  pfxlen0  41161  pfxfv  41164  pfxeq  41169  pfxsuffeqwrdeq  41171  pfxpfx  41180  ccats1pfxeq  41186  ccats1pfxeqrex  41187  pfxccatin12lem2  41189  pfxccatpfx1  41192  pfxccatid  41195  repswpfx  41201  goldbachth  41224  prmdvdsfmtnof1lem1  41261  pwdif  41266  lighneallem1  41287  lighneallem2  41288  lighneallem4a  41290  lighneallem4  41292  lighneal  41293  oexpnegnz  41354  even3prm2  41393  gbepos  41411  gbegt5  41414  gboge9  41417  sbgoldbwt  41430  nnsum3primesgbe  41445  nnsum4primeseven  41453  nnsum4primesevenALTV  41454  bgoldbtbndlem1  41458  bgoldbtbndlem2  41459  bgoldbtbndlem3  41460  tgblthelfgott  41468  tgblthelfgottOLD  41474  sprsymrelfolem2  41508  rngdir  41647  c0snmhm  41680  rngccatidALTV  41754  funcringcsetcALTV2lem6  41806  funcringcsetcALTV2lem9  41809  ringccatidALTV  41817  funcringcsetclem6ALTV  41829  ofaddmndmap  41887  mapprop  41889  nn0sumltlt  41893  gsumpr  41904  domnmsuppn0  41915  scmsuppss  41918  mndpsuppfi  41921  gsumlsscl  41929  ply1ass23l  41935  ply1mulgsumlem1  41939  lincfsuppcl  41967  linccl  41968  lincvalsng  41970  lincvalpr  41972  lincdifsn  41978  ellcoellss  41989  lincext1  42008  lincext2  42009  lincext3  42010  lindslinindimp2lem2  42013  ldepspr  42027  lincresunit3lem1  42033  lincresunit3lem2  42034  islindeps2  42037  logcxp0  42094  elbigo2r  42112  elbigolo1  42116  fllog2  42127  nnolog2flm1  42149  digvalnn0  42158  nn0digval  42159  dignn0fr  42160  dignn0ldlem  42161  dignnld  42162  digexp  42166  dignn0flhalflem1  42174  dignn0flhalflem2  42175  dignn0ehalf  42176  dignn0flhalf  42177  amgmwlem  42313
  Copyright terms: Public domain W3C validator