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

Theorem adantll 713
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 488 . 2 ((𝜃𝜑) → 𝜑)
2 adant2.1 . 2 ((𝜑𝜓) → 𝜒)
31, 2sylan 583 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:  ad2antlr  726  ad2ant2l  745  ad2ant2lr  747  ad5ant23  759  ad5ant24  760  ad5ant25  761  3adant1  1127  3ad2antl3  1184  ralcom2  3319  vtocl2d  3508  sbc2iegf  3798  sbcralt  3804  pofun  5459  poinxp  5600  xpdifid  5996  sossfld  6014  predpo  6138  preddowncl  6147  tz7.7  6189  onfr  6202  ssimaex  6727  fndmdif  6793  dffo4  6850  fcompt  6876  fconst2g  6946  f1cofveqaeq  6998  2f1fvneq  7000  isores3  7071  fvmptopab  7192  limsssuc  7549  el2mpocl  7768  1stconst  7782  2ndconst  7783  curry1  7786  curry2  7789  extmptsuppeq  7841  suppss  7847  suppssov1  7849  suppss2  7851  onnseq  7968  oe0  8134  oesuclem  8137  oecl  8149  oaordi  8159  oawordri  8163  omordi  8179  omword2  8187  omlimcl  8191  odi  8192  omass  8193  oeoe  8212  nnaordi  8231  oaabs  8258  omsmolem  8267  eceqoveq  8389  mapsnd  8437  dom2lem  8536  sbthlem9  8623  php3  8691  onomeneq  8697  isinf  8719  frfi  8751  fiint  8783  fodomfib  8786  fofinf1o  8787  marypha1lem  8885  ordiso2  8967  unwdomg  9036  xpwdomg  9037  ac5num  9451  cff1  9673  cfcoflem  9687  infpssrlem4  9721  isf32lem9  9776  isf34lem7  9794  fin1a2lem13  9827  fin1a2s  9829  hsmexlem4  9844  axdc2lem  9863  zorn2lem6  9916  axpowndlem2  10013  inttsk  10189  tskuni  10198  nqereu  10344  prcdnq  10408  addclprlem2  10432  ltexpri  10458  prlem936  10462  reclem2pr  10463  axsup  10709  add4  10853  ltleadd  11116  lt2mul2div  11511  nn2ge  11656  zextle  12047  fnn0ind  12073  xrlttr  12525  ifle  12582  xnn0lem1lt  12629  xaddass  12634  xmulasslem3  12671  xlemul1a  12673  xadddilem  12679  xrsupsslem  12692  xrinfmsslem  12693  supxrunb1  12704  supxrunb2  12705  ixxin  12747  difreicc  12866  iccsplit  12867  iccshftr  12868  iccshftl  12870  iccdil  12872  icccntr  12874  fzaddel  12940  fzadd2  12941  fzrev  12969  modadd1  13275  modmul1  13291  fsuppmapnn0fiub  13358  mulexp  13468  expadd  13471  expmul  13474  expnbnd  13593  bccl  13682  hashdom  13740  prsshashgt1  13771  hashfacen  13812  brfi1uzind  13856  wrdnval  13892  swrdccat3blem  14096  revccat  14123  2shfti  14434  rexico  14708  cau3lem  14709  subcn2  14946  caucvgb  15031  iseraltlem1  15033  sumss  15076  fsumsplitsn  15095  incexclem  15186  supcvg  15206  mertenslem2  15236  fprodn0  15328  fprodsplitsn  15338  fprodle  15345  eftlcl  15455  reeftlcl  15456  rpnnen2lem6  15567  dvdsext  15666  3dvds  15675  sqoddm1div8z  15698  gcdcllem3  15843  bezoutr1  15906  seq1st  15908  dvdslcm  15935  lcmeq0  15937  lcmcl  15938  lcmneg  15940  lcmdvds  15945  coprmgcdb  15986  dvdsprime  16024  pc2dvds  16208  prmpwdvds  16233  unbenlem  16237  infpnlem1  16239  1arith  16256  vdwmc2  16308  ramcl  16358  mrcuni  16887  isacs1i  16923  acsfn  16925  funcpropd  17165  curfcl  17477  curf2ndf  17492  resmhm  17980  resmhm2b  17982  mhmco  17983  mhmima  17984  pwsdiagmhm  17990  gsumwsubmcl  17996  gsumwspan  18006  pwmnd  18097  dfgrp2  18123  subgint  18298  ghmmhmb  18364  resghm  18369  cntzmhm  18464  symgextf1lem  18543  f1omvdconj  18569  dfod2  18686  gexdvds  18704  subgpgp  18717  sylow1lem3  18720  frgpnabllem1  18989  dprdfeq0  19140  isdrng2  19508  cntzsubr  19564  islmodd  19636  lsslss  19729  reslmhm2b  19822  psgnfix1  20290  psgndif  20294  copsgndif  20295  ocvocv  20363  frlmsslsp  20488  frlmlbs  20489  psrbaglefi  20613  mptcoe1fsupp  20847  ply1coe  20928  mamudi  21011  mamudir  21012  mat1dimelbas  21079  scmatmulcl  21126  scmatfo  21138  mulmarep1gsum2  21182  mdetunilem7  21226  mdetunilem9  21228  gsummatr01lem3  21265  smadiadetlem3  21276  cpmadugsumlemF  21484  leordtval  21821  cnpnei  21872  cnco  21874  cnss1  21884  cmpsub  22008  hauscmplem  22014  dissnlocfin  22137  ptbasid  22183  tx2cn  22218  upxp  22231  txindis  22242  xkoptsub  22262  xkopt  22263  trfbas2  22451  filconn  22491  trfil2  22495  filssufilg  22519  ufileu  22527  fixufil  22530  ufilen  22538  rnelfmlem  22560  flimclsi  22586  hauspwpwf1  22595  fclsopn  22622  fclsfnflim  22635  fclscmpi  22637  alexsubALTlem4  22658  ptcmplem5  22664  tgpmulg  22701  subgtgp  22713  tgpt0  22727  tsmsxplem2  22762  metss  23118  metustfbas  23167  dscopn  23183  xrsmopn  23420  cncfss  23507  icoopnst  23547  iccpnfcnv  23552  icccvx  23558  evth  23567  phtpycc  23599  pcohtpylem  23627  lmmbrf  23869  fgcfil  23878  caucfil  23890  cfilres  23903  bcth3  23938  cmscsscms  23980  ovolfioo  24074  ovolficc  24075  voliunlem3  24159  volcn  24213  mbflimsup  24273  mbfi1fseqlem5  24326  itg2seq  24349  bddiblnc  24448  dvnff  24529  dvnadd  24535  cpnord  24541  c1liplem1  24602  plypf1  24812  plyaddlem1  24813  plymullem1  24814  coeeulem  24824  coeidlem  24837  dgrle  24843  dgrnznn  24847  plycjlem  24876  elqaalem3  24920  ulmcaulem  24992  ulmcau  24993  psergf  25010  psercn2  25021  efopn  25252  abscxpbnd  25345  leibpi  25531  isppw2  25703  muinv  25781  bposlem3  25873  gausslemma2dlem4  25956  pntrmax  26151  pntpbnd1  26173  qabvexp  26213  eqeelen  26701  colinearalglem4  26706  axcgrid  26713  axsegconlem1  26714  axsegconlem3  26716  ax5seglem1  26725  ax5seglem2  26726  ax5seglem9  26734  axcontlem2  26762  cusgrfilem2  27249  vtxdgfisf  27269  usgr2pthlem  27555  uspgrn2crct  27597  crctcshwlkn0  27610  wwlksnext  27682  wwlksnextproplem3  27700  eupth2lem3lem4  28019  frgr3vlem1  28061  frgr3vlem2  28062  3vfriswmgrlem  28065  frgrwopreglem5  28109  numclwwlk3lem2  28172  grpoidinvlem3  28292  grpoidinv  28294  grpoideu  28295  nmoub3i  28559  nmlno0lem  28579  nmlnoubi  28582  ipasslem3  28619  ipblnfi  28641  hvaddsub4  28864  his35  28874  shsel3  29101  chj4  29321  spansncol  29354  chscllem2  29424  5oalem2  29441  3oalem2  29449  hoaddcl  29544  adjsym  29619  cnvadj  29678  hhcno  29690  hhcnf  29691  nmopub2tALT  29695  unoplin  29706  counop  29707  nmfnleub2  29712  hmoplin  29728  brafnmul  29737  nmlnop0iALT  29781  nmopun  29800  nmophmi  29817  riesz3i  29848  riesz1  29851  cnlnadjlem2  29854  cnlnadjlem6  29858  adjmul  29878  adjadd  29879  bra11  29894  cnvbraval  29896  kbass5  29906  kbass6  29907  leop2  29910  leopadd  29918  leopmuli  29919  leoptri  29922  leopnmid  29924  nmopleid  29925  pj3si  29993  hstel2  30005  cvcon3  30070  dmdmd  30086  dmdbr5  30094  mdsl0  30096  mdslmd1lem1  30111  mdslmd1lem2  30112  mdslmd3i  30118  superpos  30140  chirredlem2  30177  chirredlem3  30178  mdsymlem3  30191  mdsymlem5  30193  mdsymlem6  30194  sumdmdlem  30204  cdjreui  30218  cdj1i  30219  cdj3i  30227  foresf1o  30276  2ndimaxp  30412  abfmpel  30421  fcomptf  30424  fcnvgreu  30439  fdifsuppconst  30452  xrge0infss  30513  xnn0gt0  30523  cycpm2tr  30814  intlidl  31013  rhmpreimaprmidl  31035  lssdimle  31094  mdetpmtr1  31176  cmpcref  31203  xrge0iifcnv  31284  esumcst  31430  hasheuni  31452  esum2dlem  31459  esum2d  31460  sigaclcu2  31487  insiga  31504  unelldsys  31525  measres  31589  measdivcst  31591  volfiniune  31597  ddemeas  31603  sgn3da  31907  actfunsnf1o  31983  sconnpi1  32594  cvmsss2  32629  satfv1lem  32717  fmlaomn0  32745  gonarlem  32749  mrsubco  32876  dfon2lem6  33141  dftrpred3g  33180  poseq  33203  soseq  33204  frr1  33252  hfext  33752  elicc3  33773  fnessref  33813  bj-ismooredr2  34520  pibt2  34829  fin2solem  35036  fin2so  35037  lindsenlbs  35045  matunitlindflem1  35046  matunitlindflem2  35047  poimirlem2  35052  poimirlem14  35064  poimirlem25  35075  poimirlem26  35076  poimirlem29  35079  poimirlem30  35080  broucube  35084  heicant  35085  mblfinlem2  35088  mblfinlem3  35089  mblfinlem4  35090  ex-ovoliunnfl  35093  mbfresfi  35096  cnambfre  35098  itg2addnclem  35101  itg2addnclem2  35102  itg2addnc  35104  ftc1anclem3  35125  ftc1anclem4  35126  ftc1anclem5  35127  ftc1anclem6  35128  ftc1anclem7  35129  ftc1anclem8  35130  ftc1anc  35131  eqfnun  35153  indexdom  35165  filbcmb  35171  fdc  35176  incsequz  35179  metf1o  35186  caures  35191  bndss  35217  ismtycnv  35233  heiborlem1  35242  rrncmslem  35263  isdrngo2  35389  rngoisocnv  35412  unichnidl  35462  erim2  36064  ax12eq  36230  ax12el  36231  lshpset2N  36408  pmapglb2N  37060  pmapglb2xN  37061  pclfinN  37189  polval2N  37195  cdleme31fv2  37682  cdleme32fvcl  37729  cdleme48gfv  37826  tendoicl  38085  tendoipl  38086  diaglbN  38344  dochkr1  38767  dochkr1OLDN  38768  selvval2lem5  39419  fsuppind  39443  fsuppssind  39446  dvdsexpim  39476  nacsfix  39640  eq0rabdioph  39704  diophren  39741  rencldnfilem  39748  pell1234qrdich  39789  jm2.24  39891  jm2.26lem3  39929  wepwsolem  39973  pwssplit4  40020  isnumbasgrplem3  40036  grumnudlem  40980  cvgdvgrat  41004  ofsubid  41015  bcc0  41031  binomcxplemnn0  41040  uzwo4  41674  fiiuncl  41686  iunincfi  41717  nsstr  41718  rexanuz3  41719  iinssiin  41751  ralimda  41761  disjrnmpt2  41802  fompt  41806  disjinfi  41807  choicefi  41816  fsneq  41822  difmap  41823  iunmapsn  41833  axccdom  41840  axccd  41848  rnmptlb  41867  rnmptbd2lem  41873  ssfiunibd  41928  supxrgelem  41956  suplesup  41958  xrlexaddrp  41971  xralrple2  41973  infxrunb2  41987  xralrple3  41993  xrralrecnnle  42004  xrralrecnnge  42013  supxrunb3  42023  unb2ltle  42039  rexabslelem  42042  supminfrnmpt  42069  infxrpnf  42071  supminfxr  42090  supminfxr2  42095  xrpnf  42112  iooiinicc  42166  ressioosup  42179  iooiinioc  42180  ressiooinf  42181  fsumsupp0  42207  divcnvg  42256  limcrecl  42258  sumnnodd  42259  islpcn  42268  lptre2pt  42269  limcresiooub  42271  limcresioolb  42272  limclner  42280  fnlimfvre  42303  allbutfifvre  42304  climinf3  42345  limsupmnflem  42349  limsupre3uzlem  42364  limsupreuzmpt  42368  climuzlem  42372  climisp  42375  climrescn  42377  climxrrelem  42378  climxrre  42379  climlimsupcex  42398  liminflelimsuplem  42404  limsupgtlem  42406  liminfvalxr  42412  liminfreuzlem  42431  liminfltlem  42433  liminflimsupclim  42436  xlimpnfxnegmnf  42443  liminflbuz2  42444  liminflimsupxrre  42446  cnrefiisplem  42458  xlimmnfvlem2  42462  xlimmnfv  42463  xlimpnfvlem2  42466  xlimpnfv  42467  xlimmnfmpt  42472  xlimpnfmpt  42473  climxlim2lem  42474  dfxlim2v  42476  xlimliminflimsup  42491  cncfuni  42515  icccncfext  42516  cncficcgt0  42517  cncfiooicclem1  42522  cncfiooiccre  42524  dvasinbx  42549  dvdsn1add  42568  dvnmul  42572  dvmptfprodlem  42573  dvnprodlem1  42575  dvnprodlem3  42577  iblspltprt  42602  itgioocnicc  42606  itgspltprt  42608  ismbl3  42615  stirlinglem5  42707  dirker2re  42721  dirkerper  42725  dirkertrigeq  42730  dirkercncflem2  42733  fourierdlem12  42748  fourierdlem15  42751  fourierdlem16  42752  fourierdlem20  42756  fourierdlem21  42757  fourierdlem22  42758  fourierdlem39  42775  fourierdlem40  42776  fourierdlem41  42777  fourierdlem42  42778  fourierdlem46  42781  fourierdlem49  42784  fourierdlem50  42785  fourierdlem57  42792  fourierdlem58  42793  fourierdlem59  42794  fourierdlem64  42799  fourierdlem65  42800  fourierdlem66  42801  fourierdlem68  42803  fourierdlem70  42805  fourierdlem71  42806  fourierdlem73  42808  fourierdlem78  42813  fourierdlem79  42814  fourierdlem80  42815  fourierdlem81  42816  fourierdlem82  42817  fourierdlem83  42818  fourierdlem87  42822  fourierdlem93  42828  fourierdlem95  42830  fourierdlem101  42836  fourierdlem103  42838  fourierdlem104  42839  fourierdlem111  42846  fourierdlem112  42847  sqwvfoura  42857  fourierswlem  42859  elaa2lem  42862  etransclem13  42876  etransclem23  42886  etransclem24  42887  etransclem32  42895  etransclem38  42901  etransclem46  42909  qndenserrnbllem  42923  rrxsnicc  42929  ioorrnopnlem  42933  prsal  42947  intsal  42957  salexct  42961  dfsalgen2  42968  issalnnd  42972  sge0rnre  42990  sge0val  42992  sge0z  43001  sge0revalmpt  43004  sge0tsms  43006  sge0pr  43020  sge0resplit  43032  sge0split  43035  sge0splitmpt  43037  sge0iunmptlemfi  43039  sge0iunmptlemre  43041  sge0fodjrnlem  43042  sge0iunmpt  43044  sge0rpcpnf  43047  sge0ltfirpmpt2  43052  sge0isum  43053  sge0xaddlem1  43059  sge0xaddlem2  43060  sge0pnffsumgt  43068  sge0gtfsumgt  43069  sge0seq  43072  sge0reuz  43073  nnfoctbdjlem  43081  nnfoctbdj  43082  meadjun  43088  meadjiunlem  43091  voliunsge0lem  43098  meaiuninc3v  43110  omeiunltfirp  43145  carageniuncllem2  43148  caratheodorylem1  43152  caratheodorylem2  43153  caratheodory  43154  isomenndlem  43156  isomennd  43157  hoicvr  43174  volicorescl  43179  ovnsubaddlem2  43197  hoidmvlelem2  43222  hoidmvlelem3  43223  hoidmvle  43226  ovnhoilem2  43228  hspdifhsp  43242  hoiqssbllem2  43249  hoiqssbllem3  43250  hspmbllem2  43253  ovnsubadd2lem  43271  ovolval4lem1  43275  vonvolmbl  43287  vonioo  43308  vonicc  43311  pimrecltpos  43331  issmfle  43366  smflimlem1  43391  smflimlem2  43392  smflimlem6  43396  smfresal  43407  smfrec  43408  smfmullem4  43413  smfpimcc  43426  smflimmpt  43428  smfsuplem1  43429  smfsuplem3  43431  smfsupmpt  43433  smfsupxr  43434  smfinflem  43435  smfinfmpt  43437  smflimsuplem4  43441  smflimsuplem5  43442  smflimsupmpt  43447  smfliminfmpt  43450  smonoord  43875  lswn0  43948  poprelb  44028  fmtnoprmfac1  44069  fmtnofac2lem  44072  sbgoldbst  44283  resmgmhm  44405  resmgmhm2b  44407  mgmhmco  44408  mgmhmima  44409  snlindsntorlem  44866  1arymaptf  45042  aacllem  45316
  Copyright terms: Public domain W3C validator