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

Theorem adantll 712
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
Hypothesis
Ref Expression
adant2.1 ((𝜑𝜓) → 𝜒)
Assertion
Ref Expression
adantll (((𝜃𝜑) ∧ 𝜓) → 𝜒)

Proof of Theorem adantll
StepHypRef Expression
1 simpr 485 . 2 ((𝜃𝜑) → 𝜑)
2 adant2.1 . 2 ((𝜑𝜓) → 𝜒)
31, 2sylan 580 1 (((𝜃𝜑) ∧ 𝜓) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 206  df-an 397
This theorem is referenced by:  ad2antlr  725  ad2ant2l  744  ad2ant2lr  746  ad5ant23  758  ad5ant24  759  ad5ant25  760  3adant1  1130  3ad2antl3  1187  ralcom2  3348  vtocl2d  3511  sbc2iegf  3819  sbcralt  3826  pofun  5561  poinxp  5710  xpdifid  6118  sossfld  6136  preddowncl  6284  tz7.7  6341  onfr  6354  ssimaex  6923  fndmdif  6989  dffo4  7049  fcompt  7075  fconst2g  7148  f1cofveqaeq  7201  2f1fvneq  7203  isores3  7276  fvmptopabOLD  7408  limsssuc  7782  el2mpocl  8014  1stconst  8028  2ndconst  8029  curry1  8032  curry2  8035  poseq  8086  soseq  8087  extmptsuppeq  8115  suppss  8121  suppssOLD  8122  suppssov1  8125  suppss2  8127  onnseq  8286  oe0  8464  oesuclem  8467  oecl  8479  oaordi  8489  oawordri  8493  omordi  8509  omword2  8517  omlimcl  8521  odi  8522  omass  8523  oeoe  8542  nnaordi  8561  oaabs  8590  omsmolem  8599  eceqoveq  8757  mapsnd  8820  dom2lem  8928  sbthlem9  9031  rexdif1en  9098  php3OLD  9164  onomeneqOLD  9169  isinf  9200  isinfOLD  9201  frfi  9228  fiint  9264  fodomfib  9266  fofinf1o  9267  marypha1lem  9365  ordiso2  9447  unwdomg  9516  xpwdomg  9517  frr1  9691  ac5num  9968  cff1  10190  cfcoflem  10204  infpssrlem4  10238  isf32lem9  10293  isf34lem7  10311  fin1a2lem13  10344  fin1a2s  10346  hsmexlem4  10361  axdc2lem  10380  zorn2lem6  10433  axpowndlem2  10530  inttsk  10706  tskuni  10715  nqereu  10861  prcdnq  10925  addclprlem2  10949  ltexpri  10975  prlem936  10979  reclem2pr  10980  axsup  11226  add4  11371  ltleadd  11634  lt2mul2div  12029  nn2ge  12176  zextle  12572  fnn0ind  12598  xrlttr  13051  ifle  13108  xnn0lem1lt  13155  xaddass  13160  xmulasslem3  13197  xlemul1a  13199  xadddilem  13205  xrsupsslem  13218  xrinfmsslem  13219  supxrunb1  13230  supxrunb2  13231  ixxin  13273  difreicc  13393  iccsplit  13394  iccshftr  13395  iccshftl  13397  iccdil  13399  icccntr  13401  fzaddel  13467  fzadd2  13468  fzrev  13496  modadd1  13805  modmul1  13821  fsuppmapnn0fiub  13888  mulexp  13999  expadd  14002  expmul  14005  expnbnd  14127  bccl  14214  hashdom  14271  prsshashgt1  14302  hashfacen  14343  hashfacenOLD  14344  brfi1uzind  14389  wrdnval  14425  swrdccat3blem  14619  revccat  14646  2shfti  14957  rexico  15230  cau3lem  15231  subcn2  15469  caucvgb  15556  iseraltlem1  15558  sumss  15601  fsumsplitsn  15621  incexclem  15713  supcvg  15733  mertenslem2  15762  fprodn0  15854  fprodsplitsn  15864  fprodle  15871  eftlcl  15981  reeftlcl  15982  rpnnen2lem6  16093  dvdsext  16195  3dvds  16205  sqoddm1div8z  16228  gcdcllem3  16373  bezoutr1  16437  seq1st  16439  dvdslcm  16466  lcmeq0  16468  lcmcl  16469  lcmneg  16471  lcmdvds  16476  coprmgcdb  16517  dvdsprime  16555  pc2dvds  16743  prmpwdvds  16768  unbenlem  16772  infpnlem1  16774  1arith  16791  vdwmc2  16843  ramcl  16893  mrcuni  17493  isacs1i  17529  acsfn  17531  funcpropd  17779  curfcl  18113  curf2ndf  18128  resmhm  18623  resmhm2b  18625  mhmco  18626  mhmima  18627  pwsdiagmhm  18633  gsumwsubmcl  18639  gsumwspan  18648  pwmnd  18739  dfgrp2  18767  subgint  18943  ghmmhmb  19010  resghm  19015  cntzmhm  19110  symgextf1lem  19193  f1omvdconj  19219  dfod2  19337  gexdvds  19357  subgpgp  19370  sylow1lem3  19373  frgpnabllem1  19642  dprdfeq0  19792  isdrng2  20183  cntzsubr  20240  islmodd  20313  lsslss  20407  reslmhm2b  20500  psgnfix1  20987  psgndif  20991  copsgndif  20992  ocvocv  21060  frlmsslsp  21187  frlmlbs  21188  psrbaglefi  21319  psrbaglefiOLD  21320  mptcoe1fsupp  21570  psropprmul  21593  ply1coe  21651  mamudi  21734  mamudir  21735  mat1dimelbas  21804  scmatmulcl  21851  scmatfo  21863  mulmarep1gsum2  21907  mdetunilem7  21951  mdetunilem9  21953  gsummatr01lem3  21990  smadiadetlem3  22001  cpmadugsumlemF  22209  leordtval  22548  cnpnei  22599  cnco  22601  cnss1  22611  cmpsub  22735  hauscmplem  22741  dissnlocfin  22864  ptbasid  22910  tx2cn  22945  upxp  22958  txindis  22969  xkoptsub  22989  xkopt  22990  trfbas2  23178  filconn  23218  trfil2  23222  filssufilg  23246  ufileu  23254  fixufil  23257  ufilen  23265  rnelfmlem  23287  flimclsi  23313  hauspwpwf1  23322  fclsopn  23349  fclsfnflim  23362  fclscmpi  23364  alexsubALTlem4  23385  ptcmplem5  23391  tgpmulg  23428  subgtgp  23440  tgpt0  23454  tsmsxplem2  23489  metss  23848  metustfbas  23897  dscopn  23913  xrsmopn  24159  cncfss  24246  icoopnst  24286  iccpnfcnv  24291  icccvx  24297  evth  24306  phtpycc  24338  pcohtpylem  24366  lmmbrf  24610  fgcfil  24619  caucfil  24631  cfilres  24644  bcth3  24679  cmscsscms  24721  ovolfioo  24815  ovolficc  24816  voliunlem3  24900  volcn  24954  mbflimsup  25014  mbfi1fseqlem5  25068  itg2seq  25091  bddiblnc  25190  dvnff  25271  dvnadd  25277  cpnord  25283  c1liplem1  25344  plypf1  25557  plyaddlem1  25558  plymullem1  25559  coeeulem  25569  coeidlem  25582  dgrle  25588  dgrnznn  25592  plycjlem  25621  elqaalem3  25665  ulmcaulem  25737  ulmcau  25738  psergf  25755  psercn2  25766  efopn  25997  abscxpbnd  26090  leibpi  26276  isppw2  26448  muinv  26526  bposlem3  26618  gausslemma2dlem4  26701  pntrmax  26896  pntpbnd1  26918  qabvexp  26958  madebday  27213  eqeelen  27739  colinearalglem4  27744  axcgrid  27751  axsegconlem1  27752  axsegconlem3  27754  ax5seglem1  27763  ax5seglem2  27764  ax5seglem9  27772  axcontlem2  27800  cusgrfilem2  28290  vtxdgfisf  28310  usgr2pthlem  28597  uspgrn2crct  28639  crctcshwlkn0  28652  wwlksnext  28724  wwlksnextproplem3  28742  eupth2lem3lem4  29061  frgr3vlem1  29103  frgr3vlem2  29104  3vfriswmgrlem  29107  frgrwopreglem5  29151  numclwwlk3lem2  29214  grpoidinvlem3  29334  grpoidinv  29336  grpoideu  29337  nmoub3i  29601  nmlno0lem  29621  nmlnoubi  29624  ipasslem3  29661  ipblnfi  29683  hvaddsub4  29906  his35  29916  shsel3  30143  chj4  30363  spansncol  30396  chscllem2  30466  5oalem2  30483  3oalem2  30491  hoaddcl  30586  adjsym  30661  cnvadj  30720  hhcno  30732  hhcnf  30733  nmopub2tALT  30737  unoplin  30748  counop  30749  nmfnleub2  30754  hmoplin  30770  brafnmul  30779  nmlnop0iALT  30823  nmopun  30842  nmophmi  30859  riesz3i  30890  riesz1  30893  cnlnadjlem2  30896  cnlnadjlem6  30900  adjmul  30920  adjadd  30921  bra11  30936  cnvbraval  30938  kbass5  30948  kbass6  30949  leop2  30952  leopadd  30960  leopmuli  30961  leoptri  30964  leopnmid  30966  nmopleid  30967  pj3si  31035  hstel2  31047  cvcon3  31112  dmdmd  31128  dmdbr5  31136  mdsl0  31138  mdslmd1lem1  31153  mdslmd1lem2  31154  mdslmd3i  31160  superpos  31182  chirredlem2  31219  chirredlem3  31220  mdsymlem3  31233  mdsymlem5  31235  mdsymlem6  31236  sumdmdlem  31246  cdjreui  31260  cdj1i  31261  cdj3i  31269  foresf1o  31317  2ndimaxp  31449  abfmpel  31457  fcomptf  31460  fcnvgreu  31475  fdifsuppconst  31488  xrge0infss  31548  xnn0gt0  31557  cycpm2tr  31851  intlidl  32078  rhmpreimaprmidl  32103  lssdimle  32182  mdetpmtr1  32273  cmpcref  32300  xrge0iifcnv  32383  esumcst  32531  hasheuni  32553  esum2dlem  32560  esum2d  32561  sigaclcu2  32588  insiga  32605  unelldsys  32626  measres  32690  measdivcst  32692  volfiniune  32698  ddemeas  32704  sgn3da  33010  actfunsnf1o  33086  fnrelpredd  33562  fineqvac  33567  sconnpi1  33702  cvmsss2  33737  satfv1lem  33825  fmlaomn0  33853  gonarlem  33857  mrsubco  33984  dfon2lem6  34233  mulsid1  34378  mulsid2  34379  hfext  34735  elicc3  34756  fnessref  34796  bj-ismooredr2  35548  pibt2  35855  fin2solem  36031  fin2so  36032  lindsenlbs  36040  matunitlindflem1  36041  matunitlindflem2  36042  poimirlem2  36047  poimirlem14  36059  poimirlem25  36070  poimirlem26  36071  poimirlem29  36074  poimirlem30  36075  broucube  36079  heicant  36080  mblfinlem2  36083  mblfinlem3  36084  mblfinlem4  36085  ex-ovoliunnfl  36088  mbfresfi  36091  cnambfre  36093  itg2addnclem  36096  itg2addnclem2  36097  itg2addnc  36099  ftc1anclem3  36120  ftc1anclem4  36121  ftc1anclem5  36122  ftc1anclem6  36123  ftc1anclem7  36124  ftc1anclem8  36125  ftc1anc  36126  eqfnun  36148  indexdom  36160  filbcmb  36166  fdc  36171  incsequz  36174  metf1o  36181  caures  36186  bndss  36212  ismtycnv  36228  heiborlem1  36237  rrncmslem  36258  isdrngo2  36384  rngoisocnv  36407  unichnidl  36457  erimeq2  37107  ax12eq  37370  ax12el  37371  lshpset2N  37548  pmapglb2N  38201  pmapglb2xN  38202  pclfinN  38330  polval2N  38336  cdleme31fv2  38823  cdleme32fvcl  38870  cdleme48gfv  38967  tendoicl  39226  tendoipl  39227  diaglbN  39485  dochkr1  39908  dochkr1OLDN  39909  selvval2lem5  40645  fsuppind  40703  fsuppssind  40706  mhpind  40707  dvdsexpim  40752  zaddcomlem  40858  zmulcomlem  40862  nacsfix  40973  eq0rabdioph  41037  diophren  41074  rencldnfilem  41081  pell1234qrdich  41122  jm2.24  41225  jm2.26lem3  41263  wepwsolem  41307  pwssplit4  41354  isnumbasgrplem3  41370  onexoegt  41516  onov0suclim  41547  cantnfresb  41596  omcl2  41604  ofoaid1  41610  ofoaid2  41611  grumnudlem  42507  cvgdvgrat  42535  ofsubid  42546  bcc0  42562  binomcxplemnn0  42571  uzwo4  43203  fiiuncl  43215  iunincfi  43246  nsstr  43247  rexanuz3  43248  iinssiin  43281  disjrnmpt2  43343  fompt  43347  disjinfi  43348  choicefi  43357  fsneq  43363  difmap  43364  iunmapsn  43374  axccdom  43379  axccd  43386  rnmptlb  43406  rnmptbd2lem  43412  ssfiunibd  43479  supxrgelem  43507  suplesup  43509  xrlexaddrp  43522  xralrple2  43524  infxrunb2  43538  xralrple3  43544  xrralrecnnle  43553  xrralrecnnge  43561  supxrunb3  43570  unb2ltle  43586  rexabslelem  43589  supminfrnmpt  43616  infxrpnf  43617  supminfxr  43635  supminfxr2  43640  xrpnf  43657  pimxrneun  43660  iooiinicc  43712  ressioosup  43725  iooiinioc  43726  ressiooinf  43727  fsumsupp0  43751  divcnvg  43800  limcrecl  43802  sumnnodd  43803  islpcn  43812  lptre2pt  43813  limcresiooub  43815  limcresioolb  43816  limclner  43824  fnlimfvre  43847  allbutfifvre  43848  climinf3  43889  limsupmnflem  43893  limsupre3uzlem  43908  limsupreuzmpt  43912  climuzlem  43916  climisp  43919  climrescn  43921  climxrrelem  43922  climxrre  43923  climlimsupcex  43942  liminflelimsuplem  43948  limsupgtlem  43950  liminfvalxr  43956  liminfreuzlem  43975  liminfltlem  43977  liminflimsupclim  43980  xlimpnfxnegmnf  43987  liminflbuz2  43988  liminflimsupxrre  43990  cnrefiisplem  44002  xlimmnfvlem2  44006  xlimmnfv  44007  xlimpnfvlem2  44010  xlimpnfv  44011  xlimmnfmpt  44016  xlimpnfmpt  44017  climxlim2lem  44018  dfxlim2v  44020  xlimliminflimsup  44035  cncfuni  44059  icccncfext  44060  cncficcgt0  44061  cncfiooicclem1  44066  cncfiooiccre  44068  dvasinbx  44093  dvdsn1add  44112  dvnmul  44116  dvmptfprodlem  44117  dvnprodlem1  44119  dvnprodlem3  44121  iblspltprt  44146  itgioocnicc  44150  itgspltprt  44152  ismbl3  44159  stirlinglem5  44251  dirker2re  44265  dirkerper  44269  dirkertrigeq  44274  dirkercncflem2  44277  fourierdlem12  44292  fourierdlem15  44295  fourierdlem16  44296  fourierdlem20  44300  fourierdlem21  44301  fourierdlem22  44302  fourierdlem39  44319  fourierdlem40  44320  fourierdlem41  44321  fourierdlem42  44322  fourierdlem46  44325  fourierdlem49  44328  fourierdlem50  44329  fourierdlem57  44336  fourierdlem58  44337  fourierdlem59  44338  fourierdlem64  44343  fourierdlem65  44344  fourierdlem66  44345  fourierdlem68  44347  fourierdlem70  44349  fourierdlem71  44350  fourierdlem73  44352  fourierdlem78  44357  fourierdlem79  44358  fourierdlem80  44359  fourierdlem81  44360  fourierdlem82  44361  fourierdlem83  44362  fourierdlem87  44366  fourierdlem93  44372  fourierdlem95  44374  fourierdlem101  44380  fourierdlem103  44382  fourierdlem104  44383  fourierdlem111  44390  fourierdlem112  44391  sqwvfoura  44401  fourierswlem  44403  elaa2lem  44406  etransclem13  44420  etransclem23  44430  etransclem24  44431  etransclem32  44439  etransclem38  44445  etransclem46  44453  qndenserrnbllem  44467  rrxsnicc  44473  ioorrnopnlem  44477  prsal  44491  intsal  44503  salexct  44507  dfsalgen2  44514  issalnnd  44518  sge0rnre  44537  sge0val  44539  sge0z  44548  sge0revalmpt  44551  sge0tsms  44553  sge0pr  44567  sge0resplit  44579  sge0split  44582  sge0splitmpt  44584  sge0iunmptlemfi  44586  sge0iunmptlemre  44588  sge0fodjrnlem  44589  sge0iunmpt  44591  sge0rpcpnf  44594  sge0ltfirpmpt2  44599  sge0isum  44600  sge0xaddlem1  44606  sge0xaddlem2  44607  sge0pnffsumgt  44615  sge0gtfsumgt  44616  sge0seq  44619  sge0reuz  44620  nnfoctbdjlem  44628  nnfoctbdj  44629  meadjun  44635  meadjiunlem  44638  voliunsge0lem  44645  meaiuninc3v  44657  omeiunltfirp  44692  carageniuncllem2  44695  caratheodorylem1  44699  caratheodorylem2  44700  caratheodory  44701  isomenndlem  44703  isomennd  44704  hoicvr  44721  volicorescl  44726  ovnsubaddlem2  44744  hoidmvlelem2  44769  hoidmvlelem3  44770  hoidmvle  44773  ovnhoilem2  44775  hspdifhsp  44789  hoiqssbllem2  44796  hoiqssbllem3  44797  hspmbllem2  44800  ovnsubadd2lem  44818  ovolval4lem1  44822  vonvolmbl  44834  vonioo  44855  vonicc  44858  pimrecltpos  44881  issmfle  44918  smflimlem1  44944  smflimlem2  44945  smflimlem6  44949  smfresal  44961  smfrec  44962  smfmullem4  44967  smfpimcc  44981  smflimmpt  44983  smfsuplem1  44984  smfsuplem3  44986  smfsupmpt  44988  smfsupxr  44989  smfinflem  44990  smfinfmpt  44992  smflimsuplem4  44996  smflimsuplem5  44997  smflimsupmpt  45002  smfliminfmpt  45005  fsupdm  45015  finfdm  45019  smonoord  45495  lswn0  45568  poprelb  45648  fmtnoprmfac1  45689  fmtnofac2lem  45692  sbgoldbst  45902  resmgmhm  46024  resmgmhm2b  46026  mgmhmco  46027  mgmhmima  46028  snlindsntorlem  46483  1arymaptf  46659  ipolubdm  46944  ipoglbdm  46947  aacllem  47180
  Copyright terms: Public domain W3C validator