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

Theorem adantll 696
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 473 . 2 ((𝜃𝜑) → 𝜑)
2 adant2.1 . 2 ((𝜑𝜓) → 𝜒)
31, 2sylan 571 1 (((𝜃𝜑) ∧ 𝜓) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 198  df-an 385
This theorem is referenced by:  ad2antlr  709  ad2ant2l  743  ad2ant2lr  745  ad4ant23  752  ad4ant24  754  ad5ant23  764  ad5ant24  766  ad5ant25  768  3adant1  1153  3adant1lOLD  1215  3ad2antl3  1231  ralcom2  3303  reu6  3604  sbc2iegf  3711  sbcralt  3717  pofun  5261  poinxp  5398  xpdifid  5787  sossfld  5805  predpo  5925  preddowncl  5934  tz7.7  5976  onfr  5989  ssimaex  6494  fndmdif  6553  dffo4  6607  fcompt  6633  fconst2g  6703  f1cofveqaeq  6749  2f1fvneq  6751  isores3  6819  fvmptopab  6937  limsssuc  7290  el2mpt2cl  7494  curry1  7513  curry2  7516  extmptsuppeq  7563  suppss  7570  suppssov1  7572  suppss2  7574  suppssfv  7576  onnseq  7687  oe0  7849  oesuclem  7852  oecl  7864  oaordi  7873  oawordri  7877  oaass  7888  omordi  7893  omword2  7901  omlimcl  7905  odi  7906  omass  7907  oeoe  7926  nnaordi  7945  oaabs  7971  omsmolem  7980  eceqoveq  8098  mapsnd  8144  dom2lem  8242  sbthlem9  8327  php3  8395  onomeneq  8399  isinf  8422  frfi  8454  fiint  8486  fodomfib  8489  fofinf1o  8490  marypha1lem  8588  ordiso2  8669  unwdomg  8738  xpwdomg  8739  ac5num  9152  cff1  9375  cfcoflem  9389  infpssrlem4  9423  isf32lem9  9478  isf34lem7  9496  fin1a2lem13  9529  fin1a2s  9531  hsmexlem4  9546  axdc2lem  9565  zorn2lem6  9618  axpowndlem2  9715  inttsk  9891  tskuni  9900  nqereu  10046  prcdnq  10110  addclprlem2  10134  ltexpri  10160  prlem936  10164  reclem2pr  10165  axsup  10408  add4  10551  ltleadd  10806  lt2mul2div  11196  lediv12a  11211  nn2ge  11343  zextle  11736  fnn0ind  11762  xrlttr  12209  ifle  12266  xaddass  12317  xmulasslem3  12354  xlemul1a  12356  xadddilem  12362  xrsupsslem  12375  xrinfmsslem  12376  supxrunb1  12387  supxrunb2  12388  ixxin  12430  difreicc  12547  iccsplit  12548  iccshftr  12549  iccshftl  12551  iccdil  12553  icccntr  12555  fzaddel  12618  fzadd2  12619  fzrev  12646  modadd1  12951  modmul1  12967  fsuppmapnn0fiub  13034  mulexp  13142  expadd  13145  expmul  13148  leexp1a  13162  expnbnd  13236  bccl  13349  hashdom  13406  prsshashgt1  13435  hashfacen  13475  brfi1uzind  13517  wrdnval  13566  swrdccat3blem  13739  revccat  13759  2shfti  14063  rexico  14336  cau3lem  14337  subcn2  14568  caucvgb  14653  iseraltlem1  14655  sumss  14698  fsumsplitsn  14717  incexclem  14810  supcvg  14830  mertenslem2  14858  fprodn0  14950  fprodsplitsn  14960  fprodle  14967  eftlcl  15077  reeftlcl  15078  rpnnen2lem6  15188  dvdsext  15286  3dvds  15295  sqoddm1div8z  15318  gcdcllem3  15462  bezoutr1  15521  seq1st  15523  dvdslcm  15550  lcmeq0  15552  lcmcl  15553  lcmneg  15555  lcmdvds  15560  coprmgcdb  15601  dvdsprime  15638  pc2dvds  15820  prmpwdvds  15845  unbenlem  15849  infpnlem1  15851  1arith  15868  vdwmc2  15920  ramcl  15970  mrcuni  16506  isacs1i  16542  acsfn  16544  funcpropd  16784  natpropd  16860  curfcl  17097  curf2ndf  17112  resmhm  17584  resmhm2b  17586  mhmco  17587  mhmima  17588  pwsdiagmhm  17594  gsumwsubmcl  17600  gsumwspan  17608  dfgrp2  17672  grpissubg  17836  subgint  17840  ghmmhmb  17893  resghm  17898  cntzmhm  17992  symgextf1lem  18061  f1omvdconj  18087  pmtr3ncom  18116  dfod2  18202  gexdvds  18220  subgpgp  18233  sylow1lem3  18236  frgpnabllem1  18497  dprdfeq0  18643  isdrng2  18981  cntzsubr  19036  islmodd  19093  lsslss  19188  reslmhm2b  19281  psrbaglefi  19601  mptcoe1fsupp  19813  ply1coe  19894  psgnfix1  20172  psgndif  20176  copsgndif  20177  zrhcopsgndifOLD  20178  ocvocv  20246  frlmsslsp  20366  frlmlbs  20367  mamudi  20440  mamudir  20441  mat1dimelbas  20509  scmatmulcl  20556  scmatfo  20568  mulmarep1gsum2  20612  mdetunilem7  20656  mdetunilem9  20658  gsummatr01lem3  20696  smadiadetlem3  20707  mp2pm2mplem4  20848  chfacfisf  20893  chfacfisfcpmat  20894  cpmadugsumlemF  20915  elcls  21112  leordtval  21252  cnpnei  21303  cnco  21305  cnss1  21315  cmpsub  21438  hauscmplem  21444  dissnlocfin  21567  ptbasid  21613  tx2cn  21648  upxp  21661  txindis  21672  xkoptsub  21692  xkopt  21693  trfbas2  21881  filconn  21921  trfil2  21925  filssufilg  21949  ufileu  21957  fixufil  21960  ufilen  21968  rnelfmlem  21990  flimclsi  22016  hauspwpwf1  22025  fclsopn  22052  fclsfnflim  22065  fclscmpi  22067  alexsubALTlem3  22087  alexsubALTlem4  22088  ptcmplem5  22094  tgpmulg  22131  subgtgp  22143  tgpt0  22156  tsmsxplem2  22191  metss  22547  metustfbas  22596  dscopn  22612  xrsmopn  22849  cncfss  22936  icoopnst  22972  iccpnfcnv  22977  icccvx  22983  evth  22992  phtpycc  23024  pcohtpylem  23052  lmmbrf  23294  fgcfil  23303  caucfil  23315  cfilres  23328  bcth3  23362  ovolfioo  23471  ovolficc  23472  voliunlem3  23556  volcn  23610  mbflimsup  23670  mbfi1fseqlem5  23723  itg2seq  23746  dvnff  23923  dvnadd  23929  cpnord  23935  c1liplem1  23996  plypf1  24205  plyaddlem1  24206  plymullem1  24207  coeeulem  24217  coeidlem  24230  dgrle  24236  dgrnznn  24240  plycjlem  24269  elqaalem3  24313  ulmcaulem  24385  ulmcau  24386  psergf  24403  psercn2  24414  efopn  24641  abscxpbnd  24731  leibpi  24906  isppw2  25078  muinv  25156  bposlem3  25248  gausslemma2dlem4  25331  pntrmax  25490  pntpbnd1  25512  qabvexp  25552  eqeelen  26021  colinearalglem4  26026  axcgrid  26033  axsegconlem1  26034  axsegconlem3  26036  ax5seglem1  26045  ax5seglem2  26046  ax5seglem9  26054  axcontlem2  26082  cusgrfilem2  26603  vtxdgfisf  26623  usgr2pthlem  26910  uspgrn2crct  26952  crctcshwlkn0  26965  wwlksnextproplem3  27072  eupth2lem3lem4  27427  frgr3vlem1  27471  frgr3vlem2  27472  3vfriswmgrlem  27475  frgrwopreglem5  27519  extwwlkfablem1OLD  27540  numclwwlk3lemOLD  27592  numclwwlk3lem2  27595  grpoidinvlem3  27712  grpoidinv  27714  grpoideu  27715  nmoub3i  27979  nmlno0lem  27999  nmlnoubi  28002  ipasslem3  28039  ipblnfi  28062  hvaddsub4  28286  his35  28296  shsel3  28525  chj4  28745  spansncol  28778  chscllem2  28848  5oalem2  28865  3oalem2  28873  hoaddcl  28968  adjsym  29043  cnvadj  29102  hhcno  29114  hhcnf  29115  nmopub2tALT  29119  unoplin  29130  counop  29131  nmfnleub2  29136  hmoplin  29152  brafnmul  29161  nmlnop0iALT  29205  nmopun  29224  nmophmi  29241  riesz3i  29272  riesz1  29275  cnlnadjlem2  29278  cnlnadjlem6  29282  adjmul  29302  adjadd  29303  bra11  29318  cnvbraval  29320  kbass5  29330  kbass6  29331  leop2  29334  leopadd  29342  leopmuli  29343  leoptri  29346  leopnmid  29348  nmopleid  29349  pj3si  29417  hstel2  29429  cvcon3  29494  dmdmd  29510  dmdbr5  29518  mdsl0  29520  mdslmd1lem1  29535  mdslmd1lem2  29536  mdslmd3i  29542  superpos  29564  chirredlem2  29601  chirredlem3  29602  mdsymlem3  29615  mdsymlem5  29617  mdsymlem6  29618  sumdmdlem  29628  cdjreui  29642  cdj1i  29643  cdj3i  29651  foresf1o  29691  abfmpel  29805  fcomptf  29808  fcnvgreu  29822  xrge0infss  29875  mdetpmtr1  30237  cmpcref  30265  xrge0iifcnv  30327  esumcst  30473  hasheuni  30495  esum2dlem  30502  esum2d  30503  sigaclcu2  30531  insiga  30548  unelldsys  30569  measres  30633  measdivcst  30636  volfiniune  30641  ddemeas  30647  sgn3da  30951  actfunsnf1o  31030  sconnpi1  31566  cvmsss2  31601  mrsubco  31763  dfon2lem6  32035  dftrpred3g  32075  poseq  32096  soseq  32097  hfext  32633  elicc3  32654  fnessref  32695  fin2solem  33727  fin2so  33728  lindsenlbs  33736  matunitlindflem1  33737  matunitlindflem2  33738  poimirlem2  33743  poimirlem14  33755  poimirlem25  33766  poimirlem26  33767  poimirlem29  33770  poimirlem30  33771  broucube  33775  heicant  33776  mblfinlem2  33779  mblfinlem3  33780  mblfinlem4  33781  ex-ovoliunnfl  33784  mbfresfi  33787  cnambfre  33789  itg2addnclem  33792  itg2addnclem2  33793  itg2addnc  33795  bddiblnc  33811  ftc1anclem3  33818  ftc1anclem4  33819  ftc1anclem5  33820  ftc1anclem6  33821  ftc1anclem7  33822  ftc1anclem8  33823  ftc1anc  33824  eqfnun  33847  indexdom  33860  filbcmb  33866  fdc  33871  incsequz  33874  metf1o  33881  caures  33886  bndss  33915  ismtycnv  33931  heiborlem1  33940  rrncmslem  33961  isdrngo2  34087  rngoisocnv  34110  unichnidl  34160  ax12eq  34739  ax12el  34740  lshpset2N  34918  pmapglb2N  35570  pmapglb2xN  35571  pclfinN  35699  polval2N  35705  cdleme31fv2  36192  cdleme32fvcl  36239  cdleme48gfv  36336  tendoicl  36595  tendoipl  36596  diaglbN  36854  dochkr1  37277  dochkr1OLDN  37278  nacsfix  37795  eq0rabdioph  37860  diophren  37897  rencldnfilem  37904  pell1234qrdich  37945  jm2.24  38049  jm2.26lem3  38087  wepwsolem  38131  pwssplit4  38178  isnumbasgrplem3  38194  cvgdvgrat  39030  ofsubid  39041  bcc0  39057  binomcxplemnn0  39066  uzwo4  39732  fiiuncl  39745  iunincfi  39783  nsstr  39784  rexanuz3  39786  iinssiin  39821  ralimda  39835  disjrnmpt2  39882  fompt  39886  disjinfi  39887  choicefi  39897  fsneq  39903  difmap  39904  iunmapsn  39914  axccdom  39921  axccd  39931  rnmptlb  39955  rnmptbd2lem  39964  ssfiunibd  40022  supxrgelem  40051  suplesup  40053  xrlexaddrp  40066  xralrple2  40068  infxrunb2  40082  xralrple3  40088  xrralrecnnle  40100  xrralrecnnge  40110  supxrunb3  40120  unb2ltle  40139  rexabslelem  40142  supminfrnmpt  40169  infxrpnf  40171  supminfxr  40191  supminfxr2  40196  xrpnf  40213  iooiinicc  40267  ressioosup  40280  iooiinioc  40281  ressiooinf  40282  fsumsupp0  40308  divcnvg  40357  limcrecl  40359  sumnnodd  40360  islpcn  40369  lptre2pt  40370  limcresiooub  40372  limcresioolb  40373  limclner  40381  fnlimfvre  40404  allbutfifvre  40405  climinf3  40446  limsupmnflem  40450  limsupre3uzlem  40465  limsupreuzmpt  40469  climuzlem  40473  climisp  40476  climrescn  40478  climxrrelem  40479  climxrre  40480  climlimsupcex  40499  liminflelimsuplem  40505  limsupgtlem  40507  liminfvalxr  40513  liminfreuzlem  40532  liminfltlem  40534  liminflimsupclim  40537  cnrefiisplem  40553  xlimmnfvlem2  40557  xlimmnfv  40558  xlimpnfvlem2  40561  xlimpnfv  40562  xlimmnfmpt  40567  xlimpnfmpt  40568  climxlim2lem  40569  dfxlim2v  40571  cncfuni  40597  icccncfext  40598  cncficcgt0  40599  cncfiooicclem1  40604  cncfiooiccre  40606  dvasinbx  40633  dvdsn1add  40652  dvnmul  40656  dvmptfprodlem  40657  dvnprodlem1  40659  dvnprodlem3  40661  iblspltprt  40686  itgioocnicc  40690  itgspltprt  40692  ismbl3  40700  stirlinglem5  40792  dirker2re  40806  dirkerper  40810  dirkertrigeq  40815  dirkercncflem2  40818  fourierdlem12  40833  fourierdlem15  40836  fourierdlem16  40837  fourierdlem20  40841  fourierdlem21  40842  fourierdlem22  40843  fourierdlem39  40860  fourierdlem40  40861  fourierdlem41  40862  fourierdlem42  40863  fourierdlem46  40866  fourierdlem49  40869  fourierdlem50  40870  fourierdlem57  40877  fourierdlem58  40878  fourierdlem59  40879  fourierdlem64  40884  fourierdlem65  40885  fourierdlem66  40886  fourierdlem68  40888  fourierdlem70  40890  fourierdlem71  40891  fourierdlem73  40893  fourierdlem78  40898  fourierdlem79  40899  fourierdlem80  40900  fourierdlem81  40901  fourierdlem82  40902  fourierdlem83  40903  fourierdlem87  40907  fourierdlem93  40913  fourierdlem95  40915  fourierdlem101  40921  fourierdlem103  40923  fourierdlem104  40924  fourierdlem111  40931  fourierdlem112  40932  sqwvfoura  40942  fourierswlem  40944  elaa2lem  40947  etransclem13  40961  etransclem23  40971  etransclem24  40972  etransclem32  40980  etransclem38  40986  etransclem46  40994  qndenserrnbllem  41011  rrxsnicc  41017  ioorrnopnlem  41021  prsal  41035  intsal  41045  salexct  41049  dfsalgen2  41056  issalnnd  41060  sge0rnre  41078  sge0val  41080  sge0z  41089  sge0revalmpt  41092  sge0tsms  41094  sge0pr  41108  sge0resplit  41120  sge0split  41123  sge0splitmpt  41125  sge0iunmptlemfi  41127  sge0iunmptlemre  41129  sge0fodjrnlem  41130  sge0iunmpt  41132  sge0rpcpnf  41135  sge0ltfirpmpt2  41140  sge0isum  41141  sge0xaddlem1  41147  sge0xaddlem2  41148  sge0pnffsumgt  41156  sge0gtfsumgt  41157  sge0seq  41160  sge0reuz  41161  nnfoctbdjlem  41169  nnfoctbdj  41170  meadjun  41176  meadjiunlem  41179  voliunsge0lem  41186  meaiuninc3v  41198  omeiunltfirp  41233  carageniuncllem2  41236  caratheodorylem1  41240  caratheodorylem2  41241  caratheodory  41242  isomenndlem  41244  isomennd  41245  hoicvr  41262  volicorescl  41267  ovnsubaddlem2  41285  hoidmvlelem2  41310  hoidmvlelem3  41311  hoidmvle  41314  ovnhoilem2  41316  hspdifhsp  41330  hoiqssbllem2  41337  hoiqssbllem3  41338  hspmbllem2  41341  ovnsubadd2lem  41359  ovolval4lem1  41363  vonvolmbl  41375  vonioo  41396  vonicc  41399  pimrecltpos  41419  issmfle  41454  smflimlem1  41479  smflimlem2  41480  smflimlem6  41484  smfresal  41495  smfrec  41496  smfmullem4  41501  smfpimcc  41514  smflimmpt  41516  smfsuplem1  41517  smfsuplem3  41519  smfsupmpt  41521  smfsupxr  41522  smfinflem  41523  smfinfmpt  41525  smflimsuplem4  41529  smflimsuplem5  41530  smflimsupmpt  41535  smfliminfmpt  41538  smonoord  41934  lswn0  41973  fmtnoprmfac1  42070  fmtnofac2lem  42073  sbgoldbst  42259  resmgmhm  42384  resmgmhm2b  42386  mgmhmco  42387  mgmhmima  42388  snlindsntorlem  42845  aacllem  43136
  Copyright terms: Public domain W3C validator