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

Theorem ad2antrl 727
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 (𝜑𝜓)
21adantl 485 . 2 ((𝜒𝜑) → 𝜓)
32adantrr 716 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:  simprl  770  simprll  778  simprlr  779  simprl1  1215  simprl2  1216  simprl3  1217  disjxiun  5030  reusv2lem4  5270  axprlem5  5296  fr2nr  5501  somin1  5964  tz7.7  6189  f1oprg  6638  soisores  7063  elovmporab1w  7376  elovmporab1  7377  sorpssi  7439  onint  7494  ordsucelsuc  7521  elxp5  7614  wemoiso  7660  wemoiso2  7661  el2xptp0  7722  ressuppss  7836  imacosuppOLD  7862  tz7.48lem  8064  oalimcl  8173  oeeui  8215  oaabs2  8259  omabs  8261  swoer  8306  ralxpmap  8447  pw2f1olem  8608  enfixsn  8613  mapxpen  8671  mapunen  8674  unxpdomlem2  8711  unxpdomlem3  8712  findcard3  8749  isfinite2  8764  domunfican  8779  fodomfi  8785  fissuni  8817  fipreima  8818  indexfi  8820  fsuppsssupp  8837  marypha1lem  8885  marypha2  8891  supmo  8904  infmo  8947  oieu  8991  brwdom2  9025  ixpiunwdom  9042  cantnfval2  9120  cantnfle  9122  cantnflt  9123  cantnf  9144  wemapwe  9148  cnfcom  9151  rankonidlem  9245  r1pwcl  9264  eldju2ndl  9341  eldju2ndr  9342  djuun  9343  infxpenlem  9428  infxpenc2lem1  9434  fseqenlem1  9439  dfac8clem  9447  mappwen  9527  dfac3  9536  dfac5  9543  dfac12lem3  9560  infunsdom  9629  coftr  9688  ssfin4  9725  domfin4  9726  fin23lem26  9740  fin23lem22  9742  fin23lem28  9755  fin23lem32  9759  fin23lem40  9766  isf32lem5  9772  compssiso  9789  isf34lem4  9792  isfin1-3  9801  fin1a2lem13  9827  hsmexlem2  9842  hsmexlem4  9844  zorn2lem1  9911  ttukeylem6  9929  iundom2g  9955  konigthlem  9983  pwcfsdom  9998  fpwwe2lem12  10056  fpwwe2  10058  pwfseqlem3  10075  winalim2  10111  r1wunlim  10152  inttsk  10189  inar1  10190  grur1  10235  nqereq  10350  ltexprlem7  10457  prlem936  10462  00id  10808  addid2  10816  ltord1  11159  divdiv1  11344  divdiv2  11345  conjmul  11350  ltdivmul  11508  ledivmul  11509  lt2mul2div  11511  ltdiv23  11524  lediv23  11525  lediv12a  11526  ledivp1  11535  negfi  11581  nn0nndivcl  11958  nn0ge0div  12043  peano2uz2  12062  peano5uzi  12063  eluzp1m1  12260  qbtwnre  12584  xralrple  12590  xleadd1a  12638  xmulge0  12669  xmulass  12672  xlemul1a  12673  iooshf  12808  divelunit  12876  eluzgtdifelfzo  13098  modadd1  13275  modmul1  13291  seqcl2  13388  seqfveq2  13392  seqid2  13416  seqhomo  13417  seqdistr  13421  mulexpz  13469  leexp2r  13538  expnlbnd2  13595  expmulnbnd  13596  hashmap  13796  hashfun  13798  hashbclem  13810  hashfacen  13812  hashf1lem2  13814  hashf1  13815  ccatsymb  13931  swrdwrdsymb  14019  swrdsb0eq  14020  ccatpfx  14058  swrdswrd  14062  wrdind  14079  wrd2ind  14080  swrdccatin1  14082  swrdccatin2  14086  pfxccatin12lem2  14088  pfxccatin12  14090  swrdccat  14092  repswswrd  14141  0csh0  14150  cshwidxmod  14160  2cshw  14170  cshweqrep  14178  relexp0g  14377  relexpsucnnr  14380  relexpindlem  14418  sqrlem1  14598  sqrlem6  14603  rlim  14848  rlimclim1  14898  climsup  15022  caurcvg2  15030  caucvgb  15032  iseralt  15037  sumss  15077  fsum2dlem  15121  mptfzshft  15129  modfsummod  15145  o1fsum  15164  incexclem  15187  divrcnv  15203  flo1  15205  fprodrev  15327  fprod2dlem  15330  ruclem6  15584  moddvds  15614  dvdsaddre2b  15653  dvdsflip  15663  addmodlteqALT  15671  nn0o  15728  fldivndvdslt  15759  bitsf1ocnv  15787  bitsf1  15789  sadcaddlem  15800  bezoutlem2  15882  bezoutlem4  15884  lcmgcdlem  15944  prmind2  16023  isprm5  16045  isprm6  16052  cncongrprm  16063  hashdvds  16106  crth  16109  eulerthlem2  16113  prmdiveq  16117  hashgcdlem  16119  hashgcdeq  16120  iserodd  16166  pclem  16169  pcprendvds2  16172  pcexp  16190  pcneg  16204  pc2dvds  16209  pcmpt  16222  prmpwdvds  16234  pockthg  16236  prmreclem5  16250  4sqlem11  16285  ramub2  16344  ramubcl  16348  ram0  16352  ramub1lem2  16357  ramcl  16359  prmgaplem3  16383  prmgaplem6  16386  setscom  16523  sscpwex  17081  initoeu2  17272  setcinv  17346  funcestrcsetclem9  17394  funcsetcestrclem9  17409  fullsetcestrc  17412  1stfcl  17443  2ndfcl  17444  hofpropd  17513  isacs3lem  17772  isacs4lem  17774  acsmap2d  17785  submnd0  17936  subsubm  17977  insubm  17979  frmdup1  18025  frmdup3lem  18027  sgrp2nmndlem2  18085  isgrpinv  18152  subsubg  18298  cycsubgcl  18345  conjghm  18385  qusghm  18391  gsumwrev  18490  gsmsymgrfixlem1  18551  symgfixelsi  18559  symgsssg  18591  symgfisg  18592  psgnunilem2  18619  odf1o2  18694  sylow1lem1  18719  odcau  18725  pgpfi  18726  pgpssslw  18735  fislw  18746  efgtlen  18848  efginvrel2  18849  efgrelexlemb  18872  efgredeu  18874  efgcpbllemb  18877  frgpup1  18897  cygablOLD  19008  lt6abl  19012  gsum2d  19089  gsum2d2lem  19090  gsum2d2  19091  telgsumfzslem  19105  dmdprdsplit2lem  19164  ablfacrp  19185  pgpfac1lem3  19196  gsummgp0  19358  irredrmul  19457  subsubrg  19558  islss4  19731  lspextmo  19825  lspsnat  19914  prmirredlem  20190  znf1o  20247  znidomb  20257  frgpcyg  20269  psgnghm  20273  psgndiflemB  20293  frlmlbs  20490  frlmup1  20491  lindfind  20509  islindf3  20519  lindfmm  20520  issubassa3  20558  resspsradd  20658  resspsrmul  20659  coe1tmmul2  20909  pf1ind  20983  mamulid  21050  mat1dimelbas  21080  mdetdiaglem  21207  mdetralt2  21218  mndifsplit  21245  smadiadetglem2  21281  1elcpmat  21324  pmatcollpw3lem  21392  chfacfisf  21463  chfacfisfcpmat  21464  chfacffsupp  21465  chfacfscmulfsupp  21468  chfacfscmulgsum  21469  chfacfpmmulfsupp  21472  chfacfpmmulgsum  21473  chfacfpmmulgsum2  21474  cayhamlem1  21475  cpmadugsumlemF  21485  cayleyhamilton1  21501  tgcl  21578  pptbas  21617  clsval2  21659  mretopd  21701  lmbr2  21868  cncls2  21882  nrmsep  21966  regsep2  21985  cmpsublem  22008  cmpsub  22009  tgcmp  22010  uncmp  22012  hauscmplem  22015  iunconnlem  22036  1stcrest  22062  2ndcctbss  22064  2ndcsep  22068  dis2ndc  22069  hausllycmp  22103  dislly  22106  kgentopon  22147  1stckgen  22163  kgencn3  22167  ptpjpre1  22180  ptbasin  22186  ptpjopn  22221  dfac14  22227  ptcnplem  22230  txcn  22235  txindis  22243  txdis1cn  22244  ptrescn  22248  txcmplem1  22250  txcmp  22252  txhaus  22256  txlm  22257  tx1stc  22259  txkgen  22261  xkococn  22269  qtopcn  22323  kqreglem1  22350  kqreglem2  22351  kqnrmlem1  22352  kqnrmlem2  22353  hmeoimaf1o  22379  reghmph  22402  nrmhmph  22403  txhmeo  22412  ptuncnv  22416  filconn  22492  fbasrn  22493  fmfnfmlem2  22564  flimfnfcls  22637  cnpfcfi  22649  alexsublem  22653  alexsubALTlem2  22657  alexsubALTlem3  22658  alexsubALTlem4  22659  alexsubALT  22660  ptcmplem3  22663  cnextfval  22671  tsmsxp  22764  imasdsf1olem  22984  bl2in  23011  blssps  23035  blss  23036  blssexps  23037  blssex  23038  blcld  23116  stdbdxmet  23126  met1stc  23132  prdsxmslem2  23140  metcnp3  23151  metcnpi3  23157  txmetcnp  23158  nmo0  23345  nmoid  23352  icccmplem1  23431  icccmp  23434  xrge0tsms  23443  metdseq0  23463  cnheiborlem  23563  cnheibor  23564  cnllycmp  23565  pcoval2  23625  cmetcaulem  23896  iscmet3lem1  23899  iscmet3lem2  23900  equivcau  23908  lmcau  23921  cncmet  23930  ivthlem2  24060  ivthlem3  24061  ovoliunlem2  24111  ovolscalem2  24122  uniioombl  24197  dyaddisj  24204  opnmbllem  24209  volivth  24215  ismbfd  24247  ismbf3d  24262  mbfimaopnlem  24263  mbfinf  24273  itg1addlem4  24307  mbfi1fseqlem1  24323  mbfi1fseqlem3  24325  mbfi1fseqlem4  24326  mbfi1fseqlem5  24327  mbfi1fseqlem6  24328  itg2seq  24350  itg2lea  24352  itg2split  24357  itg2cnlem1  24369  bddiblnc  24449  limciun  24501  dvmptfsum  24582  rolle  24597  c1lip1  24604  dvcnvrelem1  24624  dvcnvre  24626  dvcvx  24627  itgsubst  24656  tdeglem4  24665  mdegmullem  24683  plyco0  24793  coemullem  24851  dgreq0  24866  dgrmul  24871  dgrco  24876  elqaalem2  24920  aannenlem1  24928  aaliou3lem9  24950  ulmres  24987  ulmshftlem  24988  angneg  25393  dcubic  25436  cxploglim  25567  cxploglim2  25568  scvxcvx  25575  lgamgulmlem5  25622  lgamcvg2  25644  ftalem2  25663  basellem3  25672  basellem4  25673  sqff1o  25771  fsumdvdsdiaglem  25772  dvdsflsumcom  25777  dvdsmulf1o  25783  fsumvma2  25802  logfac2  25805  logfacrlim  25812  logexprlim  25813  dchrelbasd  25827  lgsne0  25923  lgsqrlem2  25935  lgsqrmodndvds  25941  gausslemma2dlem1a  25953  lgseisenlem2  25964  lgsquadlem1  25968  lgsquadlem2  25969  lgsquadlem3  25970  lgsquad2lem2  25973  2sqlem8  26014  2sqlem11  26017  2sqreultlem  26035  2sqreunnltlem  26038  chpo1ubb  26069  vmadivsum  26070  rplogsumlem2  26073  rpvmasumlem  26075  dchrmusum2  26082  dchrvmasumlem1  26083  dchrisum0fno1  26099  dchrisum0re  26101  dchrisum0lem1  26104  dchrisum0lem2  26106  dchrisum0lem3  26107  dchrisum0  26108  mulogsumlem  26119  mulog2sumlem2  26123  vmalogdivsum2  26126  logsqvma  26130  log2sumbnd  26132  selberglem3  26135  selberg  26136  selberg2lem  26138  selberg2b  26140  selberg3lem2  26146  pntrmax  26152  pntrsumo1  26153  pntlemn  26188  pntlemp  26198  qabvle  26213  ostthlem1  26215  ostthlem2  26216  ostth2lem2  26222  ostth3  26226  idmot  26335  brbtwn2  26703  colinearalglem4  26707  colinearalg  26708  ax5seglem9  26735  axpaschlem  26738  axcontlem2  26763  axcontlem7  26768  axcontlem8  26769  eengtrkg  26784  upgr1eopALT  26914  uspgredg2vlem  27017  subumgr  27082  nbgr0vtxlem  27149  edgnbusgreu  27161  nb3grprlem1  27174  wlkl1loop  27431  pthdivtx  27522  usgr2pth  27557  crctcshwlkn0  27611  wlklnwwlkln1  27658  wwlksnext  27683  clwwlkccatlem  27778  clwlkclwwlklem2a  27787  clwwlkinwwlk  27829  clwwlkn1loopb  27832  clwwlkf  27836  wwlksext2clwwlk  27846  wwlksubclwwlk  27847  clwwlknscsh  27851  clwwlknon1  27886  clwwlknonex2e  27899  1conngr  27983  n4cyclfrgr  28080  numclwwlk2lem1lem  28131  2clwwlk2clwwlk  28139  numclwwlk1lem2f1  28146  numclwlk1lem1  28158  numclwwlk2lem1  28165  numclwlk2lem2f  28166  numclwwlk7  28180  frgrogt3nreg  28186  grpoidinvlem1  28291  grpoidinvlem3  28293  grporcan  28305  nmlnoubi  28583  blocnilem  28591  ipblnfi  28642  htthlem  28704  ocsh  29070  shmodsi  29176  pjhthlem2  29179  5oalem2  29442  eigposi  29623  nmopub2tALT  29696  nmfnleub2  29713  nmcexi  29813  nmopcoi  29882  kbass3  29905  mdslmd1lem1  30112  mdslmd1lem2  30113  chirredlem2  30178  chirredlem4  30180  mdsymlem3  30192  mdsymlem5  30194  sumdmdii  30202  sumdmdlem  30205  sumdmdlem2  30206  foresf1o  30277  disjxpin  30355  1stpreimas  30469  resf1o  30496  nn0xmulclb  30526  wrdt2ind  30657  xrge0tsmsd  30746  gsumvsca1  30908  gsumvsca2  30909  islinds5  30987  mdetpmtr1  31180  mdetpmtr2  31181  pstmxmet  31254  qqhghm  31343  qqhrhm  31344  esumpcvgval  31451  volmeas  31604  imambfm  31634  dya2iocnrect  31653  oddpwdc  31726  sseqf  31764  orvcgteel  31839  orvclteel  31844  ballotlemsf1o  31885  bnj1110  32368  bnj1118  32370  f1resveqaeq  32472  txpconn  32593  connpconn  32596  cnllysconn  32606  rellysconn  32612  cvmsss2  32635  cvmlift2lem9  32672  satf00  32735  fmlasuc  32747  mrsubfval  32869  mppsval  32933  dfon2lem6  33147  trpredmintr  33184  wzel  33225  fprlem1  33251  frrlem15  33256  sltres  33283  nosupno  33317  nosupbnd2  33330  sslttr  33382  ifscgr  33619  cgrxfr  33630  btwnconn1lem5  33666  btwnconn1lem6  33667  btwnconn1lem12  33673  brsegle  33683  finminlem  33780  nn0prpwlem  33784  fnessref  33819  refssfne  33820  neibastop1  33821  topjoin  33827  fnemeet2  33829  bj-prmoore  34531  bj-finsumval0  34701  topdifinffinlem  34765  lindsadd  35049  matunitlindflem2  35053  poimirlem28  35084  poimirlem32  35088  opnmbllem0  35092  mblfinlem1  35093  mblfinlem4  35096  ismblfin  35097  mbfresfi  35102  itg2addnclem  35107  itg2addnclem3  35109  itg2addnc  35110  unirep  35150  frinfm  35172  sdclem2  35179  geomcau  35196  istotbnd3  35208  sstotbnd2  35211  sstotbnd  35212  sstotbnd3  35213  totbndbnd  35226  cntotbnd  35233  ismtyres  35245  heibor1lem  35246  heiborlem1  35248  heiborlem8  35255  ismndo1  35310  isdivrngo  35387  unichnidl  35468  erim2  36070  cvlcvr1  36634  ishlat3N  36649  llnmlplnN  36834  islvol2aN  36887  4atlem4c  36896  4atlem4d  36897  isline2  37069  isline3  37071  linepsubclN  37246  lhpexle3lem  37306  lhpjat2  37316  cdlemd4  37496  cdleme0cq  37510  cdleme32fva  37732  cdleme32fvaw  37734  tendo0mul  38121  tendo0mulr  38122  diameetN  38351  dvhvaddcl  38390  dvhvaddcomN  38391  cdlemm10N  38413  dvadiaN  38423  djavalN  38430  dihvalcqat  38534  dihopelvalcpre  38543  djhval  38693  dihjat1lem  38723  metakunt15  39361  metakunt16  39362  fsuppind  39449  remul01  39538  prjspertr  39592  prjsprellsp  39598  elrfi  39628  nacsfix  39646  fzsplit1nn0  39688  eldioph2  39696  lzenom  39704  irrapxlem3  39758  pellexlem5  39767  pell1234qrne0  39787  pell1234qrmulcl  39789  pell14qrdich  39803  pell1qrge1  39804  pellqrex  39813  reglogltb  39825  reglogleb  39826  rmxypairf1o  39845  rmxycomplete  39851  monotoddzzfi  39876  congadd  39900  congsym  39902  acongrep  39914  jm2.19lem3  39925  jm2.19lem4  39926  jm2.22  39929  jm2.25  39933  expdiophlem1  39955  wepwsolem  39979  kelac1  40000  lmhmfgsplit  40023  pwslnm  40031  hbtlem6  40066  hbt  40067  mon1psubm  40143  deg1mhm  40144  iunrelexp0  40396  dssmapnvod  40714  gsumws3  40895  gsumws4  40896  mulltgt0  41644  fnchoice  41651  disjrnmpt2  41808  fzisoeu  41925  fsumiunss  42210  climinf  42241  mullimc  42251  mullimcf  42258  stoweidlem14  42649  stoweidlem17  42652  stoweidlem34  42669  stoweidlem50  42685  fourierdlem42  42784  fourierdlem62  42803  fourierdlem71  42812  fourierdlem76  42817  qndenserrnbllem  42929  subsaliuncl  42991  sge0resplit  43038  2reu8i  43662  fundcmpsurinjpreimafv  43918  iccpartigtl  43933  prproropf1olem2  44014  prproropf1olem4  44016  paireqne  44021  prmdvdsfmtnof1lem2  44095  bgoldbtbndlem3  44318  bgoldbtbnd  44320  isomushgr  44337  isomuspgrlem2c  44341  uspgrsprf1  44368  subsubmgm  44410  isassintop  44463  2zlidl  44551  2zrngnmrid  44567  rngcinv  44598  rngcinvALTV  44610  ringcinv  44649  funcringcsetcALTV2lem9  44661  ringcinvALTV  44673  funcringcsetclem9ALTV  44684  fldhmsubc  44701  fldhmsubcALTV  44719  mndpsuppss  44766  gsumlsscl  44778  lincsum  44831  lindslinindsimp1  44859  lindslinindimp2lem4  44863  lincresunitlem2  44878  elfzolborelfzop1  44921  elbigo2  44959  digexp  45014  dig1  45015  nn0sumshdiglemB  45027  1arymaptf1  45049  2arymaptf1  45060  itcoval1  45070  itcoval2  45071  itcoval3  45072  itcovalsucov  45075  ackvalsuc1mpt  45085  itschlc0xyqsol  45174
  Copyright terms: Public domain W3C validator