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

Theorem adantll 752
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 479 . 2 ((𝜃𝜑) → 𝜑)
2 adant2.1 . 2 ((𝜑𝜓) → 𝜒)
31, 2sylan 489 1 (((𝜃𝜑) ∧ 𝜓) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 197  df-an 385
This theorem is referenced by:  ad2antlr  765  ad2ant2l  799  ad2ant2lr  801  3adant1  1125  3adant1lOLD  1187  3ad2antl3  1203  ad4ant23  1211  ad4ant24  1213  ad5ant23  1222  ad5ant24  1224  ad5ant25  1226  ralcom2  3242  reu6  3536  sbc2iegf  3645  sbcralt  3651  pofun  5203  poinxp  5339  xpdifid  5720  sossfld  5738  predpo  5859  preddowncl  5868  tz7.7  5910  onfr  5924  ssimaex  6426  fndmdif  6485  dffo4  6539  foco2OLD  6544  fcompt  6564  fconst2g  6633  f1cofveqaeq  6679  2f1fvneq  6681  isores3  6749  fvmptopab  6863  limsssuc  7216  el2mpt2cl  7420  curry1  7438  curry2  7441  extmptsuppeq  7488  suppss  7495  suppssov1  7497  suppss2  7499  suppssfv  7501  onnseq  7611  oe0  7773  oesuclem  7776  oecl  7788  oaordi  7797  oawordri  7801  oaass  7812  omordi  7817  omword2  7825  omlimcl  7829  odi  7830  omass  7831  oeoe  7850  nnaordi  7869  oaabs  7895  omsmolem  7904  eceqoveq  8021  dom2lem  8163  sbthlem9  8245  php3  8313  onomeneq  8317  isinf  8340  frfi  8372  fiint  8404  fodomfib  8407  fofinf1o  8408  marypha1lem  8506  ordiso2  8587  unwdomg  8656  xpwdomg  8657  ac5num  9069  cff1  9292  cfcoflem  9306  infpssrlem4  9340  isf32lem9  9395  isf34lem7  9413  fin1a2lem13  9446  fin1a2s  9448  hsmexlem4  9463  axdc2lem  9482  zorn2lem6  9535  axpowndlem2  9632  inttsk  9808  tskuni  9817  nqereu  9963  prcdnq  10027  addclprlem2  10051  ltexpri  10077  prlem936  10081  reclem2pr  10082  axsup  10325  add4  10468  ltleadd  10723  lt2mul2div  11113  lediv12a  11128  nn2ge  11257  zextle  11662  fnn0ind  11688  xrlttr  12186  ifle  12241  xaddass  12292  xmulasslem3  12329  xlemul1a  12331  xadddilem  12337  xrsupsslem  12350  xrinfmsslem  12351  supxrunb1  12362  supxrunb2  12363  ixxin  12405  difreicc  12517  iccsplit  12518  iccshftr  12519  iccshftl  12521  iccdil  12523  icccntr  12525  fzaddel  12588  fzadd2  12589  fzrev  12616  modadd1  12921  modmul1  12937  fsuppmapnn0fiub  13004  mulexp  13113  expadd  13116  expmul  13119  leexp1a  13133  expnbnd  13207  bccl  13323  hashdom  13380  prsshashgt1  13410  hashfacen  13450  brfi1uzind  13492  wrdnval  13541  swrdccat3blem  13715  revccat  13735  2shfti  14039  rexico  14312  cau3lem  14313  subcn2  14544  caucvgb  14629  iseraltlem1  14631  sumss  14674  fsumsplitsn  14693  incexclem  14787  supcvg  14807  mertenslem2  14836  fprodn0  14928  fprodsplitsn  14939  fprodle  14946  eftlcl  15056  reeftlcl  15057  rpnnen2lem6  15167  dvdsext  15265  3dvds  15274  3dvdsOLD  15275  sqoddm1div8z  15300  gcdcllem3  15445  bezoutr1  15504  seq1st  15506  dvdslcm  15533  lcmeq0  15535  lcmcl  15536  lcmneg  15538  lcmdvds  15543  coprmgcdb  15584  dvdsprime  15622  pc2dvds  15805  prmpwdvds  15830  unbenlem  15834  infpnlem1  15836  1arith  15853  vdwmc2  15905  ramcl  15955  mrcuni  16503  isacs1i  16539  acsfn  16541  funcpropd  16781  natpropd  16857  curfcl  17093  curf2ndf  17108  resmhm  17580  resmhm2b  17582  mhmco  17583  mhmima  17584  pwsdiagmhm  17590  gsumwsubmcl  17596  gsumwspan  17604  dfgrp2  17668  grpissubg  17835  subgint  17839  ghmmhmb  17892  resghm  17897  cntzmhm  17991  symgextf1lem  18060  f1omvdconj  18086  pmtr3ncom  18115  dfod2  18201  gexdvds  18219  subgpgp  18232  sylow1lem3  18235  frgpnabllem1  18496  dprdfeq0  18641  isdrng2  18979  cntzsubr  19034  islmodd  19091  lsslss  19183  reslmhm2b  19276  psrbaglefi  19594  mptcoe1fsupp  19807  ply1coe  19888  psgnfix1  20166  psgndif  20170  zrhcopsgndif  20171  ocvocv  20237  frlmsslsp  20357  frlmlbs  20358  mamudi  20431  mamudir  20432  mat1dimelbas  20499  scmatmulcl  20546  scmatfo  20558  mulmarep1gsum2  20602  mdetunilem7  20646  mdetunilem9  20648  gsummatr01lem3  20685  smadiadetlem3  20696  mp2pm2mplem4  20836  chfacfisf  20881  chfacfisfcpmat  20882  cpmadugsumlemF  20903  elcls  21099  leordtval  21239  cnpnei  21290  cnco  21292  cnss1  21302  cmpsub  21425  hauscmplem  21431  dissnlocfin  21554  ptbasid  21600  tx2cn  21635  upxp  21648  txindis  21659  xkoptsub  21679  xkopt  21680  trfbas2  21868  filconn  21908  trfil2  21912  filssufilg  21936  ufileu  21944  fixufil  21947  ufilen  21955  rnelfmlem  21977  flimclsi  22003  hauspwpwf1  22012  fclsopn  22039  fclsfnflim  22052  fclscmpi  22054  alexsubALTlem3  22074  alexsubALTlem4  22075  ptcmplem5  22081  tgpmulg  22118  subgtgp  22130  tgpt0  22143  tsmsxplem2  22178  metss  22534  metustfbas  22583  dscopn  22599  xrsmopn  22836  cncfss  22923  icoopnst  22959  iccpnfcnv  22964  icccvx  22970  evth  22979  phtpycc  23011  pcohtpylem  23039  lmmbrf  23280  fgcfil  23289  caucfil  23301  cfilres  23314  bcth3  23348  ovolfioo  23456  ovolficc  23457  voliunlem3  23540  volcn  23594  mbflimsup  23652  mbfi1fseqlem5  23705  itg2seq  23728  dvnff  23905  dvnadd  23911  cpnord  23917  c1liplem1  23978  plypf1  24187  plyaddlem1  24188  plymullem1  24189  coeeulem  24199  coeidlem  24212  dgrle  24218  dgrnznn  24222  plycjlem  24251  elqaalem3  24295  ulmcaulem  24367  ulmcau  24368  psergf  24385  psercn2  24396  efopn  24624  abscxpbnd  24714  leibpi  24889  isppw2  25061  muinv  25139  bposlem3  25231  gausslemma2dlem4  25314  pntrmax  25473  pntpbnd1  25495  qabvexp  25535  eqeelen  26004  colinearalglem4  26009  axcgrid  26016  axsegconlem1  26017  axsegconlem3  26019  ax5seglem1  26028  ax5seglem2  26029  ax5seglem9  26037  axcontlem2  26065  cusgrfilem2  26583  vtxdgfisf  26603  usgr2pthlem  26890  uspgrn2crct  26932  crctcshwlkn0  26945  wwlksnextproplem3  27050  eupth2lem3lem4  27404  frgr3vlem1  27448  frgr3vlem2  27449  3vfriswmgrlem  27452  frgrwopreglem5  27496  extwwlkfablem1OLD  27518  numclwwlk3lemOLD  27571  numclwwlk3lem  27573  grpoidinvlem3  27690  grpoidinv  27692  grpoideu  27693  nmoub3i  27958  nmlno0lem  27978  nmlnoubi  27981  ipasslem3  28018  ipblnfi  28041  hvaddsub4  28265  his35  28275  shsel3  28504  chj4  28724  spansncol  28757  chscllem2  28827  5oalem2  28844  3oalem2  28852  hoaddcl  28947  adjsym  29022  cnvadj  29081  hhcno  29093  hhcnf  29094  nmopub2tALT  29098  unoplin  29109  counop  29110  nmfnleub2  29115  hmoplin  29131  brafnmul  29140  nmlnop0iALT  29184  nmopun  29203  nmophmi  29220  riesz3i  29251  riesz1  29254  cnlnadjlem2  29257  cnlnadjlem6  29261  adjmul  29281  adjadd  29282  bra11  29297  cnvbraval  29299  kbass5  29309  kbass6  29310  leop2  29313  leopadd  29321  leopmuli  29322  leoptri  29325  leopnmid  29327  nmopleid  29328  pj3si  29396  hstel2  29408  cvcon3  29473  dmdmd  29489  dmdbr5  29497  mdsl0  29499  mdslmd1lem1  29514  mdslmd1lem2  29515  mdslmd3i  29521  superpos  29543  chirredlem2  29580  chirredlem3  29581  mdsymlem3  29594  mdsymlem5  29596  mdsymlem6  29597  sumdmdlem  29607  cdjreui  29621  cdj1i  29622  cdj3i  29630  foresf1o  29671  abfmpel  29785  fcomptf  29788  fcnvgreu  29802  xrge0infss  29855  cmpcref  30247  xrge0iifcnv  30309  esumcst  30455  hasheuni  30477  esum2dlem  30484  esum2d  30485  sigaclcu2  30513  insiga  30530  unelldsys  30551  measres  30615  measdivcst  30618  volfiniune  30623  ddemeas  30629  sgn3da  30933  actfunsnf1o  31012  sconnpi1  31549  cvmsss2  31584  mrsubco  31746  dfon2lem6  32019  dftrpred3g  32059  poseq  32080  soseq  32081  hfext  32617  elicc3  32638  fnessref  32679  fin2solem  33726  fin2so  33727  lindsenlbs  33735  matunitlindflem1  33736  matunitlindflem2  33737  poimirlem2  33742  poimirlem14  33754  poimirlem25  33765  poimirlem26  33766  poimirlem29  33769  poimirlem30  33770  broucube  33774  heicant  33775  mblfinlem2  33778  mblfinlem3  33779  mblfinlem4  33780  ex-ovoliunnfl  33783  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  33872  incsequz  33875  metf1o  33882  caures  33887  bndss  33916  ismtycnv  33932  heiborlem1  33941  rrncmslem  33962  isdrngo2  34088  rngoisocnv  34111  unichnidl  34161  ax12eq  34748  ax12el  34749  lshpset2N  34927  pmapglb2N  35578  pmapglb2xN  35579  pclfinN  35707  polval2N  35713  cdleme31fv2  36201  cdleme32fvcl  36248  cdleme48gfv  36345  tendoicl  36604  tendoipl  36605  diaglbN  36864  dochkr1  37287  dochkr1OLDN  37288  nacsfix  37795  eq0rabdioph  37860  diophren  37897  rencldnfilem  37904  pell1234qrdich  37945  jm2.24  38050  jm2.26lem3  38088  wepwsolem  38132  pwssplit4  38179  isnumbasgrplem3  38195  cvgdvgrat  39032  ofsubid  39043  bcc0  39059  binomcxplemnn0  39068  uzwo4  39738  fiiuncl  39751  iunincfi  39789  nsstr  39790  rexanuz3  39792  iinssiin  39829  ralimda  39843  disjrnmpt2  39892  fompt  39896  disjinfi  39897  mapsnd  39905  choicefi  39909  fsneq  39915  difmap  39916  iunmapsn  39926  axccdom  39933  axccd  39946  rnmptlb  39970  rnmptbd2lem  39980  ssfiunibd  40040  supxrgelem  40069  suplesup  40071  xrlexaddrp  40084  xralrple2  40086  infxrunb2  40100  xralrple3  40106  xrralrecnnle  40118  xrralrecnnge  40129  supxrunb3  40139  unb2ltle  40158  rexabslelem  40161  supminfrnmpt  40188  infxrpnf  40190  supminfxr  40210  supminfxr2  40215  xrpnf  40232  iooiinicc  40290  ressioosup  40303  iooiinioc  40304  ressiooinf  40305  fsumsupp0  40331  divcnvg  40380  limcrecl  40382  sumnnodd  40383  islpcn  40392  lptre2pt  40393  limcresiooub  40395  limcresioolb  40396  limclner  40404  fnlimfvre  40427  allbutfifvre  40428  climinf3  40469  limsupmnflem  40473  limsupre3uzlem  40488  limsupreuzmpt  40492  climuzlem  40496  climisp  40499  climrescn  40501  climxrrelem  40502  climxrre  40503  climlimsupcex  40522  liminflelimsuplem  40528  limsupgtlem  40530  liminfvalxr  40536  liminfreuzlem  40555  liminfltlem  40557  liminflimsupclim  40560  cnrefiisplem  40576  xlimmnfvlem2  40580  xlimmnfv  40581  xlimpnfvlem2  40584  xlimpnfv  40585  xlimmnfmpt  40590  xlimpnfmpt  40591  climxlim2lem  40592  dfxlim2v  40594  cncfuni  40620  icccncfext  40621  cncficcgt0  40622  cncfiooicclem1  40627  cncfiooiccre  40629  dvasinbx  40656  dvdsn1add  40675  dvnmul  40679  dvmptfprodlem  40680  dvnprodlem1  40682  dvnprodlem3  40684  iblspltprt  40710  itgioocnicc  40714  itgspltprt  40716  ismbl3  40724  stirlinglem5  40816  dirker2re  40830  dirkerper  40834  dirkertrigeq  40839  dirkercncflem2  40842  fourierdlem12  40857  fourierdlem15  40860  fourierdlem16  40861  fourierdlem20  40865  fourierdlem21  40866  fourierdlem22  40867  fourierdlem39  40884  fourierdlem40  40885  fourierdlem41  40886  fourierdlem42  40887  fourierdlem46  40890  fourierdlem49  40893  fourierdlem50  40894  fourierdlem57  40901  fourierdlem58  40902  fourierdlem59  40903  fourierdlem64  40908  fourierdlem65  40909  fourierdlem66  40910  fourierdlem68  40912  fourierdlem70  40914  fourierdlem71  40915  fourierdlem73  40917  fourierdlem78  40922  fourierdlem79  40923  fourierdlem80  40924  fourierdlem81  40925  fourierdlem82  40926  fourierdlem83  40927  fourierdlem87  40931  fourierdlem93  40937  fourierdlem95  40939  fourierdlem101  40945  fourierdlem103  40947  fourierdlem104  40948  fourierdlem111  40955  fourierdlem112  40956  sqwvfoura  40966  fourierswlem  40968  elaa2lem  40971  etransclem13  40985  etransclem23  40995  etransclem24  40996  etransclem32  41004  etransclem38  41010  etransclem46  41018  qndenserrnbllem  41035  rrxsnicc  41041  ioorrnopnlem  41045  prsal  41059  intsal  41069  salexct  41073  dfsalgen2  41080  issalnnd  41084  sge0rnre  41102  sge0val  41104  sge0z  41113  sge0revalmpt  41116  sge0tsms  41118  sge0pr  41132  sge0resplit  41144  sge0split  41147  sge0splitmpt  41149  sge0iunmptlemfi  41151  sge0iunmptlemre  41153  sge0fodjrnlem  41154  sge0iunmpt  41156  sge0rpcpnf  41159  sge0ltfirpmpt2  41164  sge0isum  41165  sge0xaddlem1  41171  sge0xaddlem2  41172  sge0pnffsumgt  41180  sge0gtfsumgt  41181  sge0seq  41184  sge0reuz  41185  nnfoctbdjlem  41193  nnfoctbdj  41194  meadjun  41200  meadjiunlem  41203  voliunsge0lem  41210  meaiuninc3v  41222  omeiunltfirp  41257  carageniuncllem2  41260  caratheodorylem1  41264  caratheodorylem2  41265  caratheodory  41266  isomenndlem  41268  isomennd  41269  hoicvr  41286  volicorescl  41291  ovnsubaddlem2  41309  hoidmvlelem2  41334  hoidmvlelem3  41335  hoidmvle  41338  ovnhoilem2  41340  hspdifhsp  41354  hoiqssbllem2  41361  hoiqssbllem3  41362  hspmbllem2  41365  ovnsubadd2lem  41383  ovolval4lem1  41387  vonvolmbl  41399  vonioo  41420  vonicc  41423  pimrecltpos  41443  issmfle  41478  smflimlem1  41503  smflimlem2  41504  smflimlem6  41508  smfresal  41519  smfrec  41520  smfmullem4  41525  smfpimcc  41538  smflimmpt  41540  smfsuplem1  41541  smfsuplem3  41543  smfsupmpt  41545  smfsupxr  41546  smfinflem  41547  smfinfmpt  41549  smflimsuplem4  41553  smflimsuplem5  41554  smflimsupmpt  41559  smfliminfmpt  41562  smonoord  41869  lswn0  41908  fmtnoprmfac1  42005  fmtnofac2lem  42008  sbgoldbst  42194  resmgmhm  42326  resmgmhm2b  42328  mgmhmco  42329  mgmhmima  42330  snlindsntorlem  42787  aacllem  43078
  Copyright terms: Public domain W3C validator