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

Theorem ad2antrl 764
Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.)
Hypothesis
Ref Expression
ad2ant.1 (𝜑𝜓)
Assertion
Ref Expression
ad2antrl ((𝜒 ∧ (𝜑𝜃)) → 𝜓)

Proof of Theorem ad2antrl
StepHypRef Expression
1 ad2ant.1 . . 3 (𝜑𝜓)
21adantr 480 . 2 ((𝜑𝜃) → 𝜓)
32adantl 481 1 ((𝜒 ∧ (𝜑𝜃)) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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
This theorem is referenced by:  simprl  809  simprll  819  simprlr  820  disjxiun  4681  reusv2lem4  4902  fr2nr  5121  somin1  5564  tz7.7  5787  f1oprg  6219  soisores  6617  elovmpt2rab1  6923  sorpssi  6985  onint  7037  ordsucelsuc  7064  elxp5  7153  wemoiso  7195  wemoiso2  7196  el2xptp0  7256  ressuppss  7359  imacosupp  7380  tz7.48lem  7581  oalimcl  7685  oeeui  7727  oaabs2  7770  omabs  7772  swoer  7817  ralxpmap  7949  pw2f1olem  8105  enfixsn  8110  mapxpen  8167  mapunen  8170  unxpdomlem2  8206  unxpdomlem3  8207  findcard3  8244  isfinite2  8259  domunfican  8274  fodomfi  8280  fissuni  8312  fipreima  8313  indexfi  8315  fsuppsssupp  8332  marypha1lem  8380  marypha2  8386  supmo  8399  infmo  8442  oieu  8485  brwdom2  8519  ixpiunwdom  8537  cantnfval2  8604  cantnfle  8606  cantnflt  8607  cantnf  8628  wemapwe  8632  cnfcom  8635  rankonidlem  8729  r1pwcl  8748  infxpenlem  8874  infxpenc2lem1  8880  fseqenlem1  8885  dfac8clem  8893  mappwen  8973  dfac3  8982  dfac5  8989  dfac12lem3  9005  cdainf  9052  infunsdom  9074  coftr  9133  ssfin4  9170  domfin4  9171  fin23lem26  9185  fin23lem22  9187  fin23lem28  9200  fin23lem32  9204  fin23lem40  9211  isf32lem5  9217  compssiso  9234  isf34lem4  9237  isfin1-3  9246  fin1a2lem13  9272  hsmexlem2  9287  hsmexlem4  9289  zorn2lem1  9356  ttukeylem6  9374  iundom2g  9400  konigthlem  9428  pwcfsdom  9443  fpwwe2lem12  9501  fpwwe2  9503  pwfseqlem3  9520  winalim2  9556  r1wunlim  9597  inttsk  9634  inar1  9635  grur1  9680  nqereq  9795  ltexprlem7  9902  prlem936  9907  00id  10249  addid2  10257  ltord1  10592  divdiv1  10774  divdiv2  10775  conjmul  10780  ltdivmul  10936  ledivmul  10937  lt2mul2div  10939  ltdiv23  10952  lediv23  10953  lediv12a  10954  ledivp1  10963  negfi  11009  nn0nndivcl  11400  nn0ge0div  11484  peano2uz2  11503  peano5uzi  11504  eluzp1m1  11749  qbtwnre  12068  xralrple  12074  xleadd1a  12121  xmulge0  12152  xmulass  12155  xlemul1a  12156  iooshf  12290  divelunit  12352  eluzgtdifelfzo  12569  modadd1  12747  modmul1  12763  seqcl2  12859  seqfveq2  12863  seqid2  12887  seqhomo  12888  seqdistr  12892  mulexpz  12940  leexp2r  12958  expnlbnd2  13035  expmulnbnd  13036  hashmap  13260  hashfun  13262  hashbclem  13274  hashfacen  13276  hashf1lem2  13278  hashf1  13279  ccatsymb  13400  swrdsb0eq  13493  swrdswrd  13506  wrdind  13522  wrd2ind  13523  swrdccatin1  13529  swrdccatin2  13533  swrdccatin12  13537  swrdccat  13539  splid  13550  repswswrd  13577  0csh0  13585  2cshw  13605  cshweqrep  13613  relexp0g  13806  relexpsucnnr  13809  relexpindlem  13847  sqrlem1  14027  sqrlem6  14032  rlim  14270  rlimclim1  14320  climsup  14444  caurcvg2  14452  caucvgb  14454  iseralt  14459  sumss  14499  fsum2dlem  14545  mptfzshft  14554  modfsummod  14570  o1fsum  14589  incexclem  14612  divrcnv  14628  flo1  14630  fprodrev  14751  fprod2dlem  14754  ruclem6  15008  moddvds  15038  dvdsaddre2b  15076  dvdsflip  15086  addmodlteqALT  15094  nn0o  15146  fldivndvdslt  15185  bitsf1ocnv  15213  bitsf1  15215  sadcaddlem  15226  bezoutlem2  15304  bezoutlem4  15306  lcmgcdlem  15366  prmind2  15445  isprm5  15466  isprm6  15473  cncongrprm  15484  hashdvds  15527  crth  15530  eulerthlem2  15534  prmdiveq  15538  hashgcdlem  15540  hashgcdeq  15541  iserodd  15587  pclem  15590  pcprendvds2  15593  pcexp  15611  pcneg  15625  pc2dvds  15630  pcmpt  15643  prmpwdvds  15655  pockthg  15657  prmreclem5  15671  4sqlem11  15706  ramub2  15765  ramubcl  15769  ram0  15773  ramub1lem2  15778  ramcl  15780  prmgaplem3  15804  prmgaplem6  15807  setscom  15950  sscpwex  16522  initoeu2  16713  setcinv  16787  funcestrcsetclem9  16835  funcsetcestrclem9  16850  fullsetcestrc  16853  1stfcl  16884  2ndfcl  16885  hofpropd  16954  isacs3lem  17213  isacs4lem  17215  acsmap2d  17226  submnd0  17367  subsubm  17404  frmdup1  17448  frmdup3lem  17450  sgrp2nmndlem2  17458  isgrpinv  17519  subsubg  17664  cycsubgcl  17667  conjghm  17738  qusghm  17744  gsumwrev  17842  symgfixelsi  17901  symgsssg  17933  symgfisg  17934  psgnunilem2  17961  odf1o2  18034  sylow1lem1  18059  odcau  18065  pgpfi  18066  pgpssslw  18075  fislw  18086  efgtlen  18185  efginvrel2  18186  efgrelexlemb  18209  efgredeu  18211  efgcpbllemb  18214  frgpup1  18234  cygabl  18338  lt6abl  18342  gsum2d  18417  gsum2d2lem  18418  gsum2d2  18419  telgsumfzslem  18431  dmdprdsplit2lem  18490  ablfacrp  18511  pgpfac1lem3  18522  gsummgp0  18654  irredrmul  18753  subsubrg  18854  islss4  19010  lspextmo  19104  lspsnat  19193  issubassa  19372  resspsradd  19464  resspsrmul  19465  coe1tmmul2  19694  pf1ind  19767  prmirredlem  19889  znf1o  19948  znidomb  19958  frgpcyg  19970  psgnghm  19974  psgndiflemB  19994  frlmlbs  20184  frlmup1  20185  lindfind  20203  islindf3  20213  lindfmm  20214  mamulid  20295  mat1dimelbas  20325  mdetdiaglem  20452  mdetralt2  20463  mndifsplit  20490  smadiadetglem2  20526  1elcpmat  20568  pmatcollpw3lem  20636  chfacfisf  20707  chfacfisfcpmat  20708  chfacffsupp  20709  chfacfscmulfsupp  20712  chfacfscmulgsum  20713  chfacfpmmulfsupp  20716  chfacfpmmulgsum  20717  cayhamlem1  20719  cpmadugsumlemF  20729  cayleyhamilton1  20745  tgcl  20821  pptbas  20860  clsval2  20902  mretopd  20944  lmbr2  21111  cncls2  21125  nrmsep  21209  regsep2  21228  cmpsublem  21250  cmpsub  21251  tgcmp  21252  uncmp  21254  hauscmplem  21257  iunconnlem  21278  1stcrest  21304  2ndcctbss  21306  2ndcsep  21310  dis2ndc  21311  hausllycmp  21345  dislly  21348  kgentopon  21389  1stckgen  21405  kgencn3  21409  ptpjpre1  21422  ptbasin  21428  ptpjopn  21463  dfac14  21469  ptcnplem  21472  txcn  21477  txindis  21485  txdis1cn  21486  ptrescn  21490  txcmplem1  21492  txcmp  21494  txhaus  21498  txlm  21499  tx1stc  21501  txkgen  21503  xkococn  21511  qtopcn  21565  kqreglem1  21592  kqreglem2  21593  kqnrmlem1  21594  kqnrmlem2  21595  hmeoimaf1o  21621  reghmph  21644  nrmhmph  21645  txhmeo  21654  ptuncnv  21658  filconn  21734  fbasrn  21735  fmfnfmlem2  21806  flimfnfcls  21879  cnpfcfi  21891  alexsublem  21895  alexsubALTlem2  21899  alexsubALTlem3  21900  alexsubALTlem4  21901  alexsubALT  21902  ptcmplem3  21905  cnextfval  21913  tsmsxp  22005  imasdsf1olem  22225  bl2in  22252  blssps  22276  blss  22277  blssexps  22278  blssex  22279  blcld  22357  stdbdxmet  22367  met1stc  22373  prdsxmslem2  22381  metcnp3  22392  metcnpi3  22398  txmetcnp  22399  nmo0  22586  nmoid  22593  icccmplem1  22672  icccmp  22675  xrge0tsms  22684  metdseq0  22704  cnheiborlem  22800  cnheibor  22801  cnllycmp  22802  pcoval2  22862  cmetcaulem  23132  iscmet3lem1  23135  iscmet3lem2  23136  equivcau  23144  lmcau  23157  cncmet  23165  ivthlem2  23267  ivthlem3  23268  ovoliunlem2  23317  ovolscalem2  23328  uniioombl  23403  dyaddisj  23410  opnmbllem  23415  volivth  23421  ismbfd  23452  ismbf3d  23466  mbfimaopnlem  23467  mbfinf  23477  itg1addlem4  23511  mbfi1fseqlem1  23527  mbfi1fseqlem3  23529  mbfi1fseqlem4  23530  mbfi1fseqlem5  23531  mbfi1fseqlem6  23532  itg2seq  23554  itg2lea  23556  itg2split  23561  itg2cnlem1  23573  limciun  23703  dvmptfsum  23783  rolle  23798  c1lip1  23805  dvcnvrelem1  23825  dvcnvre  23827  dvcvx  23828  itgsubst  23857  tdeglem4  23865  mdegmullem  23883  plyco0  23993  coemullem  24051  dgreq0  24066  dgrmul  24071  dgrco  24076  elqaalem2  24120  aannenlem1  24128  aaliou3lem9  24150  ulmres  24187  ulmshftlem  24188  angneg  24578  dcubic  24618  cxploglim  24749  cxploglim2  24750  scvxcvx  24757  lgamgulmlem5  24804  lgamcvg2  24826  basellem3  24854  basellem4  24855  sqff1o  24953  fsumdvdsdiaglem  24954  dvdsflsumcom  24959  dvdsmulf1o  24965  fsumvma2  24984  logfac2  24987  logfacrlim  24994  logexprlim  24995  dchrelbasd  25009  lgsne0  25105  lgsqrlem2  25117  lgsqrmodndvds  25123  gausslemma2dlem1a  25135  lgseisenlem2  25146  lgsquadlem1  25150  lgsquadlem2  25151  lgsquadlem3  25152  lgsquad2lem2  25155  2sqlem8  25196  2sqlem11  25199  chpo1ubb  25215  vmadivsum  25216  rplogsumlem2  25219  rpvmasumlem  25221  dchrmusum2  25228  dchrvmasumlem1  25229  dchrisum0fno1  25245  dchrisum0re  25247  dchrisum0lem1  25250  dchrisum0lem2  25252  dchrisum0lem3  25253  dchrisum0  25254  mulogsumlem  25265  mulog2sumlem2  25269  vmalogdivsum2  25272  logsqvma  25276  log2sumbnd  25278  selberglem3  25281  selberg  25282  selberg2lem  25284  selberg2b  25286  selberg3lem2  25292  pntrmax  25298  pntrsumo1  25299  pntlemn  25334  pntlemp  25344  qabvle  25359  ostthlem1  25361  ostthlem2  25362  ostth2lem2  25368  ostth3  25372  idmot  25477  iscgra1  25747  brbtwn2  25830  colinearalglem4  25834  colinearalg  25835  ax5seglem9  25862  axpaschlem  25865  axcontlem2  25890  axcontlem7  25895  axcontlem8  25896  eengtrkg  25910  upgr1eopALT  26057  uspgredg2vlem  26160  subumgr  26225  nbgr0vtxlem  26296  edgnbusgreu  26313  nb3grprlem1  26326  wlkl1loop  26590  pthdivtx  26681  usgr2pth  26716  crctcshwlkn0  26769  wlklnwwlkln1  26822  wwlksnext  26856  clwlkclwwlklem2a  26964  clwwlkinwwlk  27003  clwwlkn1loopb  27006  clwwlkf  27010  wwlksubclwwlk  27023  clwwlknscsh  27027  clwwlknon1  27072  1conngr  27172  n4cyclfrgr  27271  numclwwlk2lem1lem  27324  clwwlkccatlem  27331  2clwwlk2clwwlk  27338  numclwlk1lem2f1  27347  numclwwlk2lem1  27356  numclwlk2lem2f  27357  numclwwlk2lem1OLD  27363  numclwlk2lem2fOLD  27364  numclwwlk7  27378  frgrogt3nreg  27384  grpoidinvlem1  27486  grpoidinvlem3  27488  grporcan  27500  nmlnoubi  27779  blocnilem  27787  ipblnfi  27839  htthlem  27902  ocsh  28270  shmodsi  28376  pjhthlem2  28379  5oalem2  28642  eigposi  28823  nmopub2tALT  28896  nmfnleub2  28913  nmcexi  29013  nmopcoi  29082  kbass3  29105  mdslmd1lem1  29312  mdslmd1lem2  29313  chirredlem2  29378  chirredlem4  29380  mdsymlem3  29392  mdsymlem5  29394  sumdmdii  29402  sumdmdlem  29405  sumdmdlem2  29406  foresf1o  29469  disjxpin  29527  1stpreimas  29611  resf1o  29633  gsumvsca1  29910  gsumvsca2  29911  xrge0tsmsd  29913  mdetpmtr1  30017  mdetpmtr2  30018  pstmxmet  30068  qqhghm  30160  qqhrhm  30161  esumpcvgval  30268  volmeas  30422  imambfm  30452  dya2iocnrect  30471  oddpwdc  30544  sseqf  30582  orvcgteel  30657  orvclteel  30662  ballotlemsf1o  30703  bnj1110  31176  bnj1118  31178  txpconn  31340  connpconn  31343  cnllysconn  31353  rellysconn  31359  cvmsss2  31382  cvmlift2lem9  31419  mrsubfval  31531  mppsval  31595  dfon2lem6  31817  trpredmintr  31855  wzel  31894  sltres  31940  nosupno  31974  nosupbnd2  31987  sslttr  32039  ifscgr  32276  cgrxfr  32287  btwnconn1lem5  32323  btwnconn1lem6  32324  btwnconn1lem12  32330  brsegle  32340  finminlem  32437  gtinfOLD  32439  nn0prpwlem  32442  fnessref  32477  refssfne  32478  neibastop1  32479  topjoin  32485  fnemeet2  32487  bj-finsumval0  33277  topdifinffinlem  33325  matunitlindflem2  33536  poimirlem28  33567  poimirlem32  33571  opnmbllem0  33575  mblfinlem1  33576  mblfinlem4  33579  ismblfin  33580  mbfresfi  33586  itg2addnclem  33591  itg2addnclem3  33593  itg2addnc  33594  bddiblnc  33610  unirep  33637  frinfm  33660  sdclem2  33668  geomcau  33685  istotbnd3  33700  sstotbnd2  33703  sstotbnd  33704  sstotbnd3  33705  totbndbnd  33718  cntotbnd  33725  ismtyres  33737  heibor1lem  33738  heiborlem1  33740  heiborlem8  33747  ismndo1  33802  isdivrngo  33879  unichnidl  33960  cvlcvr1  34944  ishlat3N  34959  llnmlplnN  35143  islvol2aN  35196  4atlem4c  35205  4atlem4d  35206  isline2  35378  isline3  35380  linepsubclN  35555  lhpexle3lem  35615  lhpjat2  35625  cdlemd4  35806  cdleme0cq  35820  cdleme32fva  36042  cdleme32fvaw  36044  tendo0mul  36431  tendo0mulr  36432  diameetN  36662  dvhvaddcl  36701  dvhvaddcomN  36702  cdlemm10N  36724  dvadiaN  36734  djavalN  36741  dihvalcqat  36845  dihopelvalcpre  36854  djhval  37004  dihjat1lem  37034  elrfi  37574  nacsfix  37592  fzsplit1nn0  37634  eldioph2  37642  lzenom  37650  irrapxlem3  37705  pellexlem5  37714  pell1234qrne0  37734  pell1234qrmulcl  37736  pell14qrdich  37750  pell1qrge1  37751  pellqrex  37760  reglogltb  37772  reglogleb  37773  rmxypairf1o  37793  rmxycomplete  37799  monotoddzzfi  37824  congadd  37850  congsym  37852  acongrep  37864  jm2.19lem3  37875  jm2.19lem4  37876  jm2.22  37879  jm2.25  37883  expdiophlem1  37905  wepwsolem  37929  kelac1  37950  lmhmfgsplit  37973  pwslnm  37981  hbtlem6  38016  hbt  38017  mon1psubm  38101  deg1mhm  38102  iunrelexp0  38311  dssmapnvod  38631  gsumws3  38816  gsumws4  38817  mulltgt0  39495  fnchoice  39502  disjrnmpt2  39689  fzisoeu  39828  fsumiunss  40125  climinf  40156  mullimc  40166  mullimcf  40173  stoweidlem14  40549  stoweidlem17  40552  stoweidlem34  40569  stoweidlem50  40585  fourierdlem42  40684  fourierdlem62  40703  fourierdlem71  40712  fourierdlem76  40717  qndenserrnbllem  40832  subsaliuncl  40894  sge0resplit  40941  iccpartigtl  41684  ccatpfx  41734  pfxccatin12lem2  41749  pfxccatin12  41750  prmdvdsfmtnof1lem2  41822  bgoldbtbndlem3  42020  bgoldbtbnd  42022  uspgrsprf1  42080  subsubmgm  42122  isassintop  42171  2zlidl  42259  2zrngnmrid  42275  rngcinv  42306  rngcinvALTV  42318  ringcinv  42357  funcringcsetcALTV2lem9  42369  ringcinvALTV  42381  funcringcsetclem9ALTV  42392  fldhmsubc  42409  fldhmsubcALTV  42427  mndpsuppss  42477  gsumlsscl  42489  lincsum  42543  lindslinindsimp1  42571  lindslinindimp2lem4  42575  lincresunitlem2  42590  elfzolborelfzop1  42634  elbigo2  42671  digexp  42726  dig1  42727  nn0sumshdiglemB  42739
  Copyright terms: Public domain W3C validator