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

Theorem adantll 710
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 208  df-an 397
This theorem is referenced by:  ad2antlr  723  ad2ant2l  742  ad2ant2lr  744  ad5ant23  756  ad5ant24  757  ad5ant25  758  3adant1  1122  3ad2antl3  1179  ralcom2w  3363  ralcom2  3364  vtocl2d  3558  sbc2iegf  3848  sbcralt  3854  pofun  5485  poinxp  5626  xpdifid  6019  sossfld  6037  predpo  6160  preddowncl  6169  tz7.7  6211  onfr  6224  ssimaex  6742  fndmdif  6805  dffo4  6862  fcompt  6888  fconst2g  6958  f1cofveqaeq  7007  2f1fvneq  7009  isores3  7077  fvmptopab  7198  limsssuc  7553  el2mpocl  7772  1stconst  7786  2ndconst  7787  curry1  7790  curry2  7793  extmptsuppeq  7845  suppss  7851  suppssov1  7853  suppss2  7855  onnseq  7972  oe0  8138  oesuclem  8141  oecl  8153  oaordi  8162  oawordri  8166  omordi  8182  omword2  8190  omlimcl  8194  odi  8195  omass  8196  oeoe  8215  nnaordi  8234  oaabs  8261  omsmolem  8270  eceqoveq  8392  mapsnd  8439  dom2lem  8538  sbthlem9  8624  php3  8692  onomeneq  8697  isinf  8720  frfi  8752  fiint  8784  fodomfib  8787  fofinf1o  8788  marypha1lem  8886  ordiso2  8968  unwdomg  9037  xpwdomg  9038  ac5num  9451  cff1  9669  cfcoflem  9683  infpssrlem4  9717  isf32lem9  9772  isf34lem7  9790  fin1a2lem13  9823  fin1a2s  9825  hsmexlem4  9840  axdc2lem  9859  zorn2lem6  9912  axpowndlem2  10009  inttsk  10185  tskuni  10194  nqereu  10340  prcdnq  10404  addclprlem2  10428  ltexpri  10454  prlem936  10458  reclem2pr  10459  axsup  10705  add4  10849  ltleadd  11112  lt2mul2div  11507  nn2ge  11653  zextle  12044  fnn0ind  12070  xrlttr  12523  ifle  12580  xnn0lem1lt  12627  xaddass  12632  xmulasslem3  12669  xlemul1a  12671  xadddilem  12677  xrsupsslem  12690  xrinfmsslem  12691  supxrunb1  12702  supxrunb2  12703  ixxin  12745  difreicc  12860  iccsplit  12861  iccshftr  12862  iccshftl  12864  iccdil  12866  icccntr  12868  fzaddel  12931  fzadd2  12932  fzrev  12960  modadd1  13266  modmul1  13282  fsuppmapnn0fiub  13349  mulexp  13458  expadd  13461  expmul  13464  expnbnd  13583  bccl  13672  hashdom  13730  prsshashgt1  13761  hashfacen  13802  brfi1uzind  13846  wrdnval  13886  swrdccat3blem  14091  revccat  14118  2shfti  14429  rexico  14703  cau3lem  14704  subcn2  14941  caucvgb  15026  iseraltlem1  15028  sumss  15071  fsumsplitsn  15090  incexclem  15181  supcvg  15201  mertenslem2  15231  fprodn0  15323  fprodsplitsn  15333  fprodle  15340  eftlcl  15450  reeftlcl  15451  rpnnen2lem6  15562  dvdsext  15661  3dvds  15670  sqoddm1div8z  15693  gcdcllem3  15840  bezoutr1  15903  seq1st  15905  dvdslcm  15932  lcmeq0  15934  lcmcl  15935  lcmneg  15937  lcmdvds  15942  coprmgcdb  15983  dvdsprime  16021  pc2dvds  16205  prmpwdvds  16230  unbenlem  16234  infpnlem1  16236  1arith  16253  vdwmc2  16305  ramcl  16355  mrcuni  16882  isacs1i  16918  acsfn  16920  funcpropd  17160  curfcl  17472  curf2ndf  17487  resmhm  17975  resmhm2b  17977  mhmco  17978  mhmima  17979  pwsdiagmhm  17985  gsumwsubmcl  17991  gsumwspan  18001  pwmnd  18042  dfgrp2  18068  subgint  18243  ghmmhmb  18309  resghm  18314  cntzmhm  18409  symgextf1lem  18479  f1omvdconj  18505  dfod2  18622  gexdvds  18640  subgpgp  18653  sylow1lem3  18656  frgpnabllem1  18924  dprdfeq0  19075  isdrng2  19443  cntzsubr  19499  islmodd  19571  lsslss  19664  reslmhm2b  19757  psrbaglefi  20082  mptcoe1fsupp  20313  ply1coe  20394  psgnfix1  20672  psgndif  20676  copsgndif  20677  ocvocv  20745  frlmsslsp  20870  frlmlbs  20871  mamudi  20942  mamudir  20943  mat1dimelbas  21010  scmatmulcl  21057  scmatfo  21069  mulmarep1gsum2  21113  mdetunilem7  21157  mdetunilem9  21159  gsummatr01lem3  21196  smadiadetlem3  21207  cpmadugsumlemF  21414  leordtval  21751  cnpnei  21802  cnco  21804  cnss1  21814  cmpsub  21938  hauscmplem  21944  dissnlocfin  22067  ptbasid  22113  tx2cn  22148  upxp  22161  txindis  22172  xkoptsub  22192  xkopt  22193  trfbas2  22381  filconn  22421  trfil2  22425  filssufilg  22449  ufileu  22457  fixufil  22460  ufilen  22468  rnelfmlem  22490  flimclsi  22516  hauspwpwf1  22525  fclsopn  22552  fclsfnflim  22565  fclscmpi  22567  alexsubALTlem4  22588  ptcmplem5  22594  tgpmulg  22631  subgtgp  22643  tgpt0  22656  tsmsxplem2  22691  metss  23047  metustfbas  23096  dscopn  23112  xrsmopn  23349  cncfss  23436  icoopnst  23472  iccpnfcnv  23477  icccvx  23483  evth  23492  phtpycc  23524  pcohtpylem  23552  lmmbrf  23794  fgcfil  23803  caucfil  23815  cfilres  23828  bcth3  23863  cmscsscms  23905  ovolfioo  23997  ovolficc  23998  voliunlem3  24082  volcn  24136  mbflimsup  24196  mbfi1fseqlem5  24249  itg2seq  24272  dvnff  24449  dvnadd  24455  cpnord  24461  c1liplem1  24522  plypf1  24731  plyaddlem1  24732  plymullem1  24733  coeeulem  24743  coeidlem  24756  dgrle  24762  dgrnznn  24766  plycjlem  24795  elqaalem3  24839  ulmcaulem  24911  ulmcau  24912  psergf  24929  psercn2  24940  efopn  25168  abscxpbnd  25261  leibpi  25448  isppw2  25620  muinv  25698  bposlem3  25790  gausslemma2dlem4  25873  pntrmax  26068  pntpbnd1  26090  qabvexp  26130  eqeelen  26618  colinearalglem4  26623  axcgrid  26630  axsegconlem1  26631  axsegconlem3  26633  ax5seglem1  26642  ax5seglem2  26643  ax5seglem9  26651  axcontlem2  26679  cusgrfilem2  27166  vtxdgfisf  27186  usgr2pthlem  27472  uspgrn2crct  27514  crctcshwlkn0  27527  wwlksnext  27599  wwlksnextproplem3  27618  eupth2lem3lem4  27938  frgr3vlem1  27980  frgr3vlem2  27981  3vfriswmgrlem  27984  frgrwopreglem5  28028  numclwwlk3lem2  28091  grpoidinvlem3  28211  grpoidinv  28213  grpoideu  28214  nmoub3i  28478  nmlno0lem  28498  nmlnoubi  28501  ipasslem3  28538  ipblnfi  28560  hvaddsub4  28783  his35  28793  shsel3  29020  chj4  29240  spansncol  29273  chscllem2  29343  5oalem2  29360  3oalem2  29368  hoaddcl  29463  adjsym  29538  cnvadj  29597  hhcno  29609  hhcnf  29610  nmopub2tALT  29614  unoplin  29625  counop  29626  nmfnleub2  29631  hmoplin  29647  brafnmul  29656  nmlnop0iALT  29700  nmopun  29719  nmophmi  29736  riesz3i  29767  riesz1  29770  cnlnadjlem2  29773  cnlnadjlem6  29777  adjmul  29797  adjadd  29798  bra11  29813  cnvbraval  29815  kbass5  29825  kbass6  29826  leop2  29829  leopadd  29837  leopmuli  29838  leoptri  29841  leopnmid  29843  nmopleid  29844  pj3si  29912  hstel2  29924  cvcon3  29989  dmdmd  30005  dmdbr5  30013  mdsl0  30015  mdslmd1lem1  30030  mdslmd1lem2  30031  mdslmd3i  30037  superpos  30059  chirredlem2  30096  chirredlem3  30097  mdsymlem3  30110  mdsymlem5  30112  mdsymlem6  30113  sumdmdlem  30123  cdjreui  30137  cdj1i  30138  cdj3i  30146  foresf1o  30193  abfmpel  30329  fcomptf  30332  fcnvgreu  30347  xrge0infss  30411  xnn0gt0  30421  cycpm2tr  30689  lssdimle  30906  mdetpmtr1  30988  cmpcref  31014  xrge0iifcnv  31076  esumcst  31222  hasheuni  31244  esum2dlem  31251  esum2d  31252  sigaclcu2  31279  insiga  31296  unelldsys  31317  measres  31381  measdivcst  31383  volfiniune  31389  ddemeas  31395  sgn3da  31699  actfunsnf1o  31775  sconnpi1  32384  cvmsss2  32419  satfv1lem  32507  fmlaomn0  32535  gonarlem  32539  mrsubco  32666  dfon2lem6  32931  dftrpred3g  32970  poseq  32993  soseq  32994  frr1  33042  hfext  33542  elicc3  33563  fnessref  33603  bj-ismooredr2  34297  pibt2  34581  fin2solem  34760  fin2so  34761  lindsenlbs  34769  matunitlindflem1  34770  matunitlindflem2  34771  poimirlem2  34776  poimirlem14  34788  poimirlem25  34799  poimirlem26  34800  poimirlem29  34803  poimirlem30  34804  broucube  34808  heicant  34809  mblfinlem2  34812  mblfinlem3  34813  mblfinlem4  34814  ex-ovoliunnfl  34817  mbfresfi  34820  cnambfre  34822  itg2addnclem  34825  itg2addnclem2  34826  itg2addnc  34828  bddiblnc  34844  ftc1anclem3  34851  ftc1anclem4  34852  ftc1anclem5  34853  ftc1anclem6  34854  ftc1anclem7  34855  ftc1anclem8  34856  ftc1anc  34857  eqfnun  34880  indexdom  34892  filbcmb  34898  fdc  34903  incsequz  34906  metf1o  34913  caures  34918  bndss  34947  ismtycnv  34963  heiborlem1  34972  rrncmslem  34993  isdrngo2  35119  rngoisocnv  35142  unichnidl  35192  erim2  35793  ax12eq  35959  ax12el  35960  lshpset2N  36137  pmapglb2N  36789  pmapglb2xN  36790  pclfinN  36918  polval2N  36924  cdleme31fv2  37411  cdleme32fvcl  37458  cdleme48gfv  37555  tendoicl  37814  tendoipl  37815  diaglbN  38073  dochkr1  38496  dochkr1OLDN  38497  selvval2lem5  39017  dvdsexpim  39061  nacsfix  39189  eq0rabdioph  39253  diophren  39290  rencldnfilem  39297  pell1234qrdich  39338  jm2.24  39440  jm2.26lem3  39478  wepwsolem  39522  pwssplit4  39569  isnumbasgrplem3  39585  grumnudlem  40501  cvgdvgrat  40525  ofsubid  40536  bcc0  40552  binomcxplemnn0  40561  uzwo4  41195  fiiuncl  41207  iunincfi  41240  nsstr  41241  rexanuz3  41242  iinssiin  41275  ralimda  41286  disjrnmpt2  41329  fompt  41333  disjinfi  41334  choicefi  41343  fsneq  41349  difmap  41350  iunmapsn  41360  axccdom  41367  axccd  41375  rnmptlb  41394  rnmptbd2lem  41400  ssfiunibd  41456  supxrgelem  41485  suplesup  41487  xrlexaddrp  41500  xralrple2  41502  infxrunb2  41516  xralrple3  41522  xrralrecnnle  41533  xrralrecnnge  41542  supxrunb3  41552  unb2ltle  41569  rexabslelem  41572  supminfrnmpt  41599  infxrpnf  41601  supminfxr  41620  supminfxr2  41625  xrpnf  41642  iooiinicc  41698  ressioosup  41711  iooiinioc  41712  ressiooinf  41713  fsumsupp0  41739  divcnvg  41788  limcrecl  41790  sumnnodd  41791  islpcn  41800  lptre2pt  41801  limcresiooub  41803  limcresioolb  41804  limclner  41812  fnlimfvre  41835  allbutfifvre  41836  climinf3  41877  limsupmnflem  41881  limsupre3uzlem  41896  limsupreuzmpt  41900  climuzlem  41904  climisp  41907  climrescn  41909  climxrrelem  41910  climxrre  41911  climlimsupcex  41930  liminflelimsuplem  41936  limsupgtlem  41938  liminfvalxr  41944  liminfreuzlem  41963  liminfltlem  41965  liminflimsupclim  41968  xlimpnfxnegmnf  41975  liminflbuz2  41976  liminflimsupxrre  41978  cnrefiisplem  41990  xlimmnfvlem2  41994  xlimmnfv  41995  xlimpnfvlem2  41998  xlimpnfv  41999  xlimmnfmpt  42004  xlimpnfmpt  42005  climxlim2lem  42006  dfxlim2v  42008  xlimliminflimsup  42023  cncfuni  42049  icccncfext  42050  cncficcgt0  42051  cncfiooicclem1  42056  cncfiooiccre  42058  dvasinbx  42085  dvdsn1add  42104  dvnmul  42108  dvmptfprodlem  42109  dvnprodlem1  42111  dvnprodlem3  42113  iblspltprt  42138  itgioocnicc  42142  itgspltprt  42144  ismbl3  42152  stirlinglem5  42244  dirker2re  42258  dirkerper  42262  dirkertrigeq  42267  dirkercncflem2  42270  fourierdlem12  42285  fourierdlem15  42288  fourierdlem16  42289  fourierdlem20  42293  fourierdlem21  42294  fourierdlem22  42295  fourierdlem39  42312  fourierdlem40  42313  fourierdlem41  42314  fourierdlem42  42315  fourierdlem46  42318  fourierdlem49  42321  fourierdlem50  42322  fourierdlem57  42329  fourierdlem58  42330  fourierdlem59  42331  fourierdlem64  42336  fourierdlem65  42337  fourierdlem66  42338  fourierdlem68  42340  fourierdlem70  42342  fourierdlem71  42343  fourierdlem73  42345  fourierdlem78  42350  fourierdlem79  42351  fourierdlem80  42352  fourierdlem81  42353  fourierdlem82  42354  fourierdlem83  42355  fourierdlem87  42359  fourierdlem93  42365  fourierdlem95  42367  fourierdlem101  42373  fourierdlem103  42375  fourierdlem104  42376  fourierdlem111  42383  fourierdlem112  42384  sqwvfoura  42394  fourierswlem  42396  elaa2lem  42399  etransclem13  42413  etransclem23  42423  etransclem24  42424  etransclem32  42432  etransclem38  42438  etransclem46  42446  qndenserrnbllem  42460  rrxsnicc  42466  ioorrnopnlem  42470  prsal  42484  intsal  42494  salexct  42498  dfsalgen2  42505  issalnnd  42509  sge0rnre  42527  sge0val  42529  sge0z  42538  sge0revalmpt  42541  sge0tsms  42543  sge0pr  42557  sge0resplit  42569  sge0split  42572  sge0splitmpt  42574  sge0iunmptlemfi  42576  sge0iunmptlemre  42578  sge0fodjrnlem  42579  sge0iunmpt  42581  sge0rpcpnf  42584  sge0ltfirpmpt2  42589  sge0isum  42590  sge0xaddlem1  42596  sge0xaddlem2  42597  sge0pnffsumgt  42605  sge0gtfsumgt  42606  sge0seq  42609  sge0reuz  42610  nnfoctbdjlem  42618  nnfoctbdj  42619  meadjun  42625  meadjiunlem  42628  voliunsge0lem  42635  meaiuninc3v  42647  omeiunltfirp  42682  carageniuncllem2  42685  caratheodorylem1  42689  caratheodorylem2  42690  caratheodory  42691  isomenndlem  42693  isomennd  42694  hoicvr  42711  volicorescl  42716  ovnsubaddlem2  42734  hoidmvlelem2  42759  hoidmvlelem3  42760  hoidmvle  42763  ovnhoilem2  42765  hspdifhsp  42779  hoiqssbllem2  42786  hoiqssbllem3  42787  hspmbllem2  42790  ovnsubadd2lem  42808  ovolval4lem1  42812  vonvolmbl  42824  vonioo  42845  vonicc  42848  pimrecltpos  42868  issmfle  42903  smflimlem1  42928  smflimlem2  42929  smflimlem6  42933  smfresal  42944  smfrec  42945  smfmullem4  42950  smfpimcc  42963  smflimmpt  42965  smfsuplem1  42966  smfsuplem3  42968  smfsupmpt  42970  smfsupxr  42971  smfinflem  42972  smfinfmpt  42974  smflimsuplem4  42978  smflimsuplem5  42979  smflimsupmpt  42984  smfliminfmpt  42987  smonoord  43412  lswn0  43451  poprelb  43533  fmtnoprmfac1  43574  fmtnofac2lem  43577  sbgoldbst  43790  resmgmhm  43912  resmgmhm2b  43914  mgmhmco  43915  mgmhmima  43916  snlindsntorlem  44423  aacllem  44800
  Copyright terms: Public domain W3C validator