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

Theorem 3ad2ant3 1104
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 481 . 2 ((𝜃𝜑) → 𝜒)
323adant1 1099 1 ((𝜓𝜃𝜑) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1054
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 385  df-3an 1056
This theorem is referenced by:  simp3l  1109  simp3r  1110  simp31  1117  simp32  1118  simp33  1119  simp3ll  1152  simp3lr  1153  simp3rl  1154  simp3rr  1155  simp3l1  1186  simp3l2  1187  simp3l3  1188  simp3r1  1189  simp3r2  1190  simp3r3  1191  simp31l  1204  simp31r  1205  simp32l  1206  simp32r  1207  simp33l  1208  simp33r  1209  simp311  1228  simp312  1229  simp313  1230  simp321  1231  simp322  1232  simp323  1233  simp331  1234  simp332  1235  simp333  1236  3anim123i  1266  3jaao  1436  ceqsalt  3259  ceqsralt  3260  vtoclgftOLD  3286  disjtpsn  4283  disjtp2  4284  elpwdifsn  4352  ssprsseq  4389  tpssi  4401  prnebg  4420  poltletr  5563  predeq123  5719  predpo  5736  funprgOLD  5979  funtpgOLD  5981  fntpg  5986  funcnvpr  5988  funcnvtp  5989  ftpg  6463  fsnunf  6492  fsnunfv  6494  fvpr1g  6499  fvpr2g  6500  fpropnf1  6564  weniso  6644  ovmpt3rab1  6933  epne3  7022  limsuc  7091  oteqimp  7229  el2xptp0  7256  funsssuppss  7366  smoel  7502  smoord  7507  omwordi  7696  oneo  7706  oeord  7713  oewordi  7716  nnmwordi  7760  nnneo  7776  uniinqs  7870  undifixp  7986  enfixsn  8110  domss2  8160  domssex2  8161  unxpdomlem3  8207  dif1en  8234  rneqdmfinf1o  8283  mapfien2  8355  dffi2  8370  unwdomg  8530  ixpiunwdom  8537  en3lplem1  8549  oemapvali  8619  fodomfi2  8921  infcdaabs  9066  infunabs  9067  infdif  9069  ackbij1lem9  9088  ackbij1lem16  9095  coflim  9121  cfsmolem  9130  isfin2-2  9179  fin1a2lem9  9268  hsmexlem2  9287  axcc2lem  9296  axcc3  9298  domtriomlem  9302  axdc3lem4  9313  axcclem  9317  zornn0g  9365  axacndlem4  9470  axacndlem5  9471  axacnd  9472  gchdomtri  9489  fpwwe  9506  tskssel  9617  tskint  9645  tskurn  9649  gruurn  9658  gruixp  9669  grudomon  9677  gruina  9678  adderpqlem  9814  mulerpqlem  9815  addassnq  9818  mulassnq  9819  distrnq  9821  ltsonq  9829  ltanq  9831  ltmnq  9832  reclem3pr  9909  dedekind  10238  addid2  10257  addcan2  10259  divdir  10748  divcan5  10765  ltdiv1  10925  infrelb  11046  lt2halves  11305  zdivmul  11487  ledivge1le  11939  addlelt  11980  xaddass  12117  xleadd1  12123  xltadd1  12124  xmulasslem3  12154  xmulass  12155  xlemul1  12158  xlemul2  12159  xltmul1  12160  xadddir  12164  elioo5  12269  iccsupr  12304  iccneg  12331  icoshft  12332  icoshftf1o  12333  iccsplit  12343  zltaddlt1le  12362  fzen  12396  ssfzunsn  12425  elfz1b  12447  fzrevral  12463  fzshftral  12466  elfz0ubfz0  12482  elfz0fzfz0  12483  fz0fzelfz0  12484  fz0fzdiffz0  12487  elfzo  12511  elfzonlteqm1  12583  ltdifltdiv  12675  modabs  12743  modcyc  12745  modaddmulmod  12777  moddi  12778  modsubdir  12779  expdiv  12951  leexp2a  12956  bcval3  13133  hashnnn0genn0  13171  hashgadd  13204  hashunx  13213  hashfun  13262  hashres  13263  hash2prd  13295  hashtpg  13305  fun2dmnop0  13314  brfi1indlem  13316  ccatval1  13395  ccatval2  13396  ccatval3  13397  ccatsymb  13400  ccatass  13406  ccats1val2  13447  swrdval2  13465  swrd0len0  13482  swrd0fv  13485  swrdeq  13490  swrdspsleq  13495  2swrdeqwrdeq  13499  swrdswrdlem  13505  swrdswrd  13506  swrd0swrd  13507  ccats1swrdeq  13515  ccats1swrdeqrex  13524  swrdccatin12lem2  13535  swrdccat3b  13542  swrdccatid  13543  splval  13548  repswswrd  13577  cshwidxmod  13595  cshwidx0mod  13597  cshf1  13602  cshwleneq  13609  scshwfzeqfzo  13618  cshimadifsn  13621  cshimadifsn0  13622  ccatco  13627  cshco  13628  swrdco  13629  f1oun2prg  13708  swrds2  13731  eqwrds3  13750  trclfvss  13791  elicc4abs  14103  mulcn2  14370  fsumsplitsnun  14528  fsumsplitsnunOLD  14530  modfsummods  14569  prodfrec  14671  ntrivcvgfvn0  14675  binomrisefac  14817  demoivreALT  14975  rpnnen2lem4  14990  dvdsval2  15030  dvdsmodexp  15035  modmulconst  15060  dvdsexp  15096  oddge22np1  15120  modremain  15179  mulgcd  15312  mulgcdr  15314  gcddiv  15315  rpmulgcd  15322  rplpwr  15323  lcmfn0val  15383  lcmftp  15396  lcmfunsnlem2lem1  15398  lcmfunsnlem2lem2  15399  lcmfunsnlem2  15400  coprmdvds  15413  cncongr1  15428  dvdsnprmd  15450  prmexpb  15477  rpexp  15479  cncongrprm  15484  modprm0  15557  modprmn0modprm0  15559  coprimeprodsq  15560  pythagtriplem1  15568  pythagtriplem3  15570  pythagtriplem10  15572  pythagtriplem6  15573  pythagtriplem11  15577  pythagtriplem12  15578  pythagtriplem13  15579  pythagtriplem15  15581  pythagtriplem17  15583  pythagtriplem19  15585  pcdvdsb  15620  dvdsprmpweqle  15637  pcfaclem  15649  vdwapun  15725  ramval  15759  0ram2  15772  0ramcl  15774  fvprmselgcd1  15796  prmgaplem6  15807  setsstructOLD  15946  imasaddvallem  16236  imasvscaval  16245  mreiincl  16303  mremre  16311  mrieqv2d  16346  cofurid  16598  initoeu2lem0  16710  initoeu2lem2  16712  funcestrcsetclem6  16832  funcestrcsetclem9  16835  funcsetcestrclem6  16847  funcsetcestrclem9  16850  xpcpropd  16895  clatleglb  17173  ress0g  17366  gsumccat  17425  gsumccatsn  17427  sgrp2nmndlem3  17459  sgrp2nmndlem5  17463  dfgrp3lem  17560  mulgdirlem  17619  mulgp1  17621  mulgmodid  17628  eqglact  17692  fvcosymgeq  17895  gsmsymgreqlem2  17897  pmtrprfv3  17920  pmtr3ncomlem1  17939  mndodcongi  18008  oddvdsnn0  18009  odngen  18038  gexnnod  18049  lsmlub  18124  lsmass  18129  efgsval2  18192  efgsrel  18193  ghmplusg  18295  odadd1  18297  odadd2  18298  srg1zr  18575  dvrcan1  18737  dvrcan3  18738  irredrmul  18753  srngadd  18905  srngmul  18906  rmodislmodlem  18978  rmodislmod  18979  lmhmvsca  19093  reslmhm2  19101  pwssplit3  19109  lbspss  19130  lsmsp  19134  lspsneu  19171  lidldvgen  19303  assa2ass  19370  evlsval  19567  evlsval2  19568  psropprmul  19656  coe1add  19682  coe1addfv  19683  coe1subfv  19684  coe1tm  19691  coe1sclmul  19700  coe1sclmul2  19702  coe1fzgsumdlem  19719  lply1binom  19724  evl1gsumdlem  19768  zrhpsgninv  19979  zrhpsgnevpm  19985  zrhpsgnodpm  19986  psgndiflemB  19994  cssmre  20085  frlmup4  20188  islindf2  20201  lindsind2  20206  f1lindf  20209  lindsss  20211  f1linds  20212  lindsmm  20215  lbslcic  20228  mndvcl  20245  mndvass  20246  mhmvlin  20251  matecl  20279  matvscacell  20290  mamulid  20295  mamurid  20296  mattposm  20313  madetsumid  20315  matepmcl  20316  matepm2cl  20317  mat1dimbas  20326  mavmulsolcl  20405  mulmarep1el  20426  mulmarep1gsum1  20427  mulmarep1gsum2  20428  1marepvsma1  20437  m1detdiag  20451  mdetdiaglem  20452  mdetdiag  20453  mdetunilem7  20472  mdetunilem9  20474  mdetmul  20477  gsummatr01lem3  20511  gsummatr01lem4  20512  gsummatr01  20513  smadiadetglem2  20526  matinv  20531  slesolinv  20534  cramerimplem1  20537  cramerimp  20540  cramerlem1  20541  pmatcoe1fsupp  20554  mat2pmatbas  20579  decpmatmullem  20624  pmatcollpw3lem  20636  chpscmat  20695  iuncld  20897  clsss  20906  ntrcls0  20928  iscldtop  20947  neiss  20961  neips  20965  restcldi  21025  cnpnei  21116  cnconst2  21135  cnpresti  21140  sslm  21151  cnt0  21198  cnt1  21202  cnhaus  21206  cncmp  21243  cmpcld  21253  cnconn  21273  conncompss  21284  ssref  21363  elptr  21424  upxp  21474  qtoptop2  21550  ordthmeolem  21652  opnfbas  21693  isfil2  21707  fbasweak  21716  snfbas  21717  fgss  21724  fgcl  21729  fbasrn  21735  trnei  21743  cfinfil  21744  csdfil  21745  supfil  21746  filufint  21771  fin1aufil  21783  fmval  21794  fmf  21796  elfm  21798  elfm3  21801  imaelfm  21802  rnelfmlem  21803  rnelfm  21804  flimclslem  21835  flfneii  21843  cnpfcfi  21891  alexsubALT  21902  ptcmplem3  21905  ustref  22069  ustelimasn  22073  utop3cls  22102  ressusp  22116  cfiluexsm  22141  prdsxmetlem  22220  txmetcn  22400  nmmtri  22473  nmrtri  22475  unitnmn0  22519  nminvr  22520  nmotri  22590  nghmplusg  22591  isclmi  22923  isclmp  22943  ncvsi  22997  fmcfil  23116  srabn  23202  rrxmvallem  23233  itgconst  23630  dvn2bss  23738  deg1mul3  23920  deg1mul3le  23921  deg1tmle  23922  q1peqb  23959  r1pcl  23962  r1pdeglt  23963  r1pid  23964  dvdsq1p  23965  dvdsr1p  23966  ptolemy  24293  sincosq1eq  24309  logeq0im1  24369  logmul2  24407  logdiv2  24408  cxplt2  24489  logbchbase  24554  relogbreexp  24558  relogbexp  24563  pythag  24592  lgamgulmlem1  24800  bcmono  25047  efexple  25051  lgsdirnn0  25114  gausslemma2dlem1a  25135  gausslemma2dlem3  25138  2lgslem1a1  25159  2lgsoddprmlem1  25178  2lgsoddprmlem2  25179  selberglem3  25281  brbtwn2  25830  axcgrid  25841  ax5seglem1  25853  ax5seglem2  25854  ax5seg  25863  axpasch  25866  axlowdimlem16  25882  axcontlem7  25895  structiedg0val  25956  lpvtx  26008  incistruhgr  26019  upgredg2vtx  26081  upgredgpr  26082  edglnl  26083  ausgrumgri  26107  ausgrusgri  26108  usgredg2vtxeuALT  26159  ushgredgedg  26166  ushgredgedgloop  26168  uspgr1v1eop  26186  usgr1v0edg  26194  uhgrissubgr  26212  egrsubgr  26214  0uhgrsubgr  26216  nbupgrres  26310  nb3grprlem1  26326  cplgr3v  26387  umgr2v2enb1  26478  finsumvtxdgeven  26504  vtxdgoddnumeven  26505  rusgrnumwrdl2  26538  rusgr1vtx  26540  isewlk  26554  ewlkinedg  26556  upgrewlkle2  26558  wlkvtxeledg  26575  wlkeq  26585  wlkl1loop  26590  wlk1walk  26591  uspgr2wlkeq  26598  uspgr2wlkeq2  26599  wlksoneq1eq2  26616  wlkonl1iedg  26617  wlkon2n0  26618  wlkres  26623  wlkp1lem8  26633  lfgriswlk  26641  lfgrwlknloop  26642  spthonpthon  26703  spthonepeq  26704  uhgrwkspth  26707  usgr2wlkspth  26711  usgr2pth  26716  wwlknp  26791  wwlknvtx  26793  wwlknlsw  26796  0enwwlksnge1  26818  wwlksnred  26855  wwlksnredwwlkn  26858  wwlksnextsur  26863  wlksnwwlknvbij  26871  wwlksnextproplem1  26872  wwlksnwwlksnon  26878  wspthsnwspthsnon  26879  umgr2adedgwlkonALT  26912  umgr2wlkon  26915  umgrwwlks2on  26923  elwspths2spth  26934  rusgr0edg  26940  rusgrnumwwlks  26941  clwwisshclwwslemlem  26970  clwwlkinwwlk  27003  loopclwwlkn1b  27005  clwwlkf  27010  clwwlkext2edg  27020  wwlksext2clwwlk  27021  clwlksfclwwlk  27049  clwlksf1clwwlklem2  27053  clwlksf1clwwlklem  27055  clwwlknon1  27072  clwwlknonwwlknonbOLD  27081  clwwlknonex2lem2  27083  clwwlknonex2  27084  clwwlknun  27087  clwwlkvbij  27088  clwwlkvbijOLD  27089  clwwlknunOLD  27091  1ewlk  27093  0clwlkv  27109  1pthon2v  27131  3wlkdlem9  27146  uhgr3cyclex  27160  umgr3cyclex  27161  upgr4cycl4dv4e  27163  upgreupthseg  27187  eupth2lem3lem6  27211  eulercrct  27220  nfrgr2v  27252  frgr3vlem1  27253  3vfriswmgr  27258  extwwlkfablem1OLD  27323  numclwwlk2lem1lem  27324  2clwwlk2clwwlklem2lem2  27329  numclwlk1lem2foalem  27341  extwwlkfab  27342  numclwlk1lem2foa  27344  numclwlk1lem2f1  27347  numclwlk1lem2fo  27348  numclwwlk1  27351  numclwwlk2lem1  27356  numclwlk2lem2f  27357  numclwlk2lem2f1o  27359  numclwwlk2  27361  numclwwlk2lem1OLD  27363  numclwlk2lem2fOLD  27364  numclwlk2lem2f1oOLD  27366  numclwwlk2OLD  27368  numclwwlk3  27372  numclwwlk5lem  27374  numclwwlk6  27377  frgrreggt1  27380  frgrreg  27381  frgrregord013  27382  vcidOLD  27547  vcdi  27548  vcdir  27549  vcass  27550  imsmetlem  27673  0oval  27771  ajval  27845  shlub  28401  hmopco  29010  adjlnop  29073  mdslmd4i  29320  fcoinvbr  29545  fresf1o  29561  divnumden2  29692  ressnm  29779  ress1r  29917  smatfval  29989  pstmfval  30067  pl1cn  30129  ind1  30207  ind0  30208  sigaclcuni  30309  sigagenss2  30341  measun  30402  measvuni  30405  dya2iocnrect  30471  omsmeas  30513  ballotlemieq  30706  ballotlemrv1  30710  sgn3da  30731  bnj837  30957  bnj517  31081  bnj553  31094  bnj594  31108  bnj967  31141  bnj1097  31175  bnj1110  31176  bnj1118  31178  bnj1128  31184  bnj1125  31186  bnj1145  31187  bnj1136  31191  bnj1173  31196  bnj1189  31203  bnj1204  31206  bnj1279  31212  bnj1321  31221  bnj1413  31229  erdszelem2  31300  cnpconn  31338  cvmscld  31381  mrsubcv  31533  mrsubvr  31534  iprodefisumlem  31752  dvdspw  31762  dfon2lem3  31814  dfon2lem7  31818  nosupfv  31977  nosupres  31978  noetalem1  31988  btwndiff  32259  brcolinear2  32290  btwnconn1  32333  nn0prpwlem  32442  hmeoclda  32453  hmeocldb  32454  ivthALT  32455  fnemeet1  32486  fnejoin1  32488  nnssi3  32580  nndivsub  32581  bj-ceqsalt1  32999  bj-evalidval  33156  onsucuni3  33345  curfv  33519  lindsdom  33533  lindsenlbs  33534  ftc1anclem4  33618  areacirclem2  33631  areacirclem5  33634  areacirc  33635  upixp  33654  filbcmb  33665  cnresima  33693  smprngopr  33981  igenval2  33995  brxrn  34276  xrnresex  34304  lsmsat  34613  lsmsatcv  34615  lsatcvatlem  34654  islshpcv  34658  l1cvpat  34659  lfli  34666  lshpset2N  34724  cvrnbtwn  34876  meetat2  34902  atcmp  34916  atcvreq0  34919  atlatmstc  34924  cvlcvr1  34944  cvlcvrp  34945  cvlatcvr2  34947  cvr2N  35015  cvratlem  35025  2atjm  35049  athgt  35060  2lplnmN  35163  2llnmj  35164  2lplnmj  35226  dalemswapyzps  35294  dalem23  35300  dalem24  35301  dalem25  35302  dalem27  35303  dalem28  35304  dalem38  35314  dalem39  35315  dalem44  35320  dalem45  35321  dalem51  35327  dalem52  35328  dalem56  35332  pmapglbx  35373  pmapjat1  35457  pmapjat2  35458  paddatclN  35553  osumcllem4N  35563  osumcllem7N  35566  ltrncoval  35749  cdleme0aa  35815  cdleme0b  35817  cdleme8  35855  cdlemesner  35901  cdleme22eALTN  35950  cdleme26eALTN  35966  cdleme35h  36061  cdleme50trn2  36156  cdleme  36165  tgrpov  36353  tendotp  36366  tendoidcl  36374  tendo0co2  36393  cdlemkvcl  36447  dvhopvadd  36699  dvhopellsm  36723  dihmeetlem1N  36896  dihmeetlem9N  36921  dihatexv  36944  lcfl7lem  37105  mapdrvallem2  37251  mapdh9a  37396  hdmapevec  37444  ismrcd1  37578  istopclsd  37580  ismrc  37581  mapfzcons  37596  eldioph2  37642  diophrex  37656  diophren  37694  pellexlem1  37710  pellexlem5  37714  pellqrexplicit  37758  reglogmul  37774  reglogexp  37775  rmxycomplete  37799  congmul  37851  congabseq  37858  acongsym  37860  acongneg2  37861  fzneg  37866  acongeq  37867  jm2.19  37877  jm2.22  37879  jm2.23  37880  jm2.20nn  37881  rmydioph  37898  rmxdiophlem  37899  jm3.1  37904  pwssplit4  37976  hbtlem2  38011  idomrootle  38090  pwinfi2  38184  relexpaddss  38327  trclimalb2  38335  brtrclfv2  38336  trclfvdecomr  38337  ntrclsneine0lem  38679  ntrclsk2  38683  ntrclsk3  38685  ntrclsk13  38686  ntrclsk4  38687  gneispace  38749  dvconstbi  38850  expgrowth  38851  chordthmALT  39483  restuni3  39615  wessf1ornlem  39685  disjf1o  39692  elrnmpt2id  39741  funimassd  39745  infnsuprnmpt  39779  infrnmptle  39963  fmul01lt1lem1  40134  climsuselem1  40157  climsuse  40158  limcperiod  40178  lptre2pt  40190  climbddf  40237  limsupvaluz2  40288  supcnvlimsup  40290  cncfshift  40405  cncfperiod  40410  icccncfext  40418  dvnmptconst  40474  dvnprodlem1  40479  dvnprodlem2  40480  iblspltprt  40507  itgspltprt  40513  stoweidlem3  40538  stoweidlem16  40551  stoweidlem17  40552  stoweidlem26  40561  stoweidlem34  40569  stoweidlem57  40592  fourierdlem41  40683  fourierdlem42  40684  fourierdlem52  40693  fourierdlem54  40695  fourierdlem74  40715  fourierdlem75  40716  fourierdlem80  40721  fourierdlem94  40735  fourierdlem102  40743  fourierdlem114  40755  etransclem18  40787  etransclem29  40798  etransclem46  40815  rrxtopnfi  40824  subsaliuncl  40894  sge0f1o  40917  sge0xp  40964  meadjiunlem  41000  voliunsge0lem  41007  volmea  41009  carageniuncllem1  41056  caratheodorylem1  41061  caratheodory  41063  isomenndlem  41065  hoicvr  41083  ovnsubaddlem2  41106  hoidmvlelem1  41130  hoidmvlelem2  41131  hoidmvlelem3  41132  hspmbllem2  41162  smfaddlem1  41292  smfco  41330  smfsuplem1  41338  2leaddle2  41637  ssfz12  41649  fsumsplitsndif  41668  fsummmodsndifre  41669  fsummmodsnunz  41670  iccpartiltu  41683  icceuelpart  41697  pfxnd  41720  pfxlen0  41721  pfxfv  41724  pfxeq  41729  pfxsuffeqwrdeq  41731  pfxpfx  41740  ccats1pfxeq  41746  ccats1pfxeqrex  41747  pfxccatin12lem2  41749  pfxccatpfx1  41752  pfxccatid  41755  repswpfx  41761  goldbachth  41784  prmdvdsfmtnof1lem1  41821  pwdif  41826  lighneallem1  41847  lighneallem2  41848  lighneallem4a  41850  lighneallem4  41852  lighneal  41853  oexpnegnz  41914  even3prm2  41953  gbepos  41971  gbegt5  41974  gboge9  41977  sbgoldbwt  41990  nnsum3primesgbe  42005  nnsum4primeseven  42013  nnsum4primesevenALTV  42014  bgoldbtbndlem1  42018  bgoldbtbndlem2  42019  bgoldbtbndlem3  42020  tgblthelfgott  42028  tgblthelfgottOLD  42034  sprsymrelfolem2  42068  rngdir  42207  c0snmhm  42240  rngccatidALTV  42314  funcringcsetcALTV2lem6  42366  funcringcsetcALTV2lem9  42369  ringccatidALTV  42377  funcringcsetclem6ALTV  42389  ofaddmndmap  42447  mapprop  42449  nn0sumltlt  42453  gsumpr  42464  domnmsuppn0  42475  scmsuppss  42478  mndpsuppfi  42481  gsumlsscl  42489  ply1ass23l  42495  ply1mulgsumlem1  42499  lincfsuppcl  42527  linccl  42528  lincvalsng  42530  lincvalpr  42532  lincdifsn  42538  ellcoellss  42549  lincext1  42568  lincext2  42569  lincext3  42570  lindslinindimp2lem2  42573  ldepspr  42587  lincresunit3lem1  42593  lincresunit3lem2  42594  islindeps2  42597  logcxp0  42654  elbigo2r  42672  elbigolo1  42676  fllog2  42687  nnolog2flm1  42709  digvalnn0  42718  nn0digval  42719  dignn0fr  42720  dignn0ldlem  42721  dignnld  42722  digexp  42726  dignn0flhalflem1  42734  dignn0flhalflem2  42735  dignn0ehalf  42736  dignn0flhalf  42737  amgmwlem  42876
  Copyright terms: Public domain W3C validator