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

Theorem adantll 750
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 476 . 2 ((𝜃𝜑) → 𝜑)
2 adant2.1 . 2 ((𝜑𝜓) → 𝜒)
31, 2sylan 487 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  763  ad2ant2l  797  ad2ant2lr  799  3ad2antl3  1245  ad4ant23  1325  ad4ant24  1327  ad5ant23  1338  ad5ant25  1342  3adant1l  1358  ralcom2  3133  reu6  3428  sbc2iegf  3537  sbcralt  3543  pofun  5080  poinxp  5216  xpdifid  5597  sossfld  5615  predpo  5736  preddowncl  5745  tz7.7  5787  onfr  5801  ssimaex  6302  fndmdif  6361  dffo4  6415  foco2OLD  6420  fcompt  6440  fconst2g  6509  f1cofveqaeq  6555  2f1fvneq  6557  isores3  6625  fvmptopab  6739  limsssuc  7092  el2mpt2cl  7296  curry1  7314  curry2  7317  extmptsuppeq  7364  suppss  7370  suppssov1  7372  suppss2  7374  suppssfv  7376  onnseq  7486  oe0  7647  oesuclem  7650  oecl  7662  oaordi  7671  oawordri  7675  oaass  7686  omordi  7691  omword2  7699  omlimcl  7703  odi  7704  omass  7705  oeoe  7724  nnaordi  7743  oaabs  7769  omsmolem  7778  eceqoveq  7895  dom2lem  8037  sbthlem9  8119  php3  8187  onomeneq  8191  isinf  8214  frfi  8246  fiint  8278  fodomfib  8281  fofinf1o  8282  marypha1lem  8380  ordiso2  8461  unwdomg  8530  xpwdomg  8531  ac5num  8897  cff1  9118  cfcoflem  9132  infpssrlem4  9166  isf32lem9  9221  isf34lem7  9239  fin1a2lem13  9272  fin1a2s  9274  hsmexlem4  9289  axdc2lem  9308  zorn2lem6  9361  axpowndlem2  9458  inttsk  9634  tskuni  9643  nqereu  9789  prcdnq  9853  addclprlem2  9877  ltexpri  9903  prlem936  9907  reclem2pr  9908  axsup  10151  add4  10294  ltleadd  10549  lt2mul2div  10939  lediv12a  10954  nn2ge  11083  zextle  11488  fnn0ind  11514  xrlttr  12011  ifle  12066  xaddass  12117  xmulasslem3  12154  xlemul1a  12156  xadddilem  12162  xrsupsslem  12175  xrinfmsslem  12176  supxrunb1  12187  supxrunb2  12188  ixxin  12230  difreicc  12342  iccsplit  12343  iccshftr  12344  iccshftl  12346  iccdil  12348  icccntr  12350  fzaddel  12413  fzadd2  12414  fzrev  12441  modadd1  12747  modmul1  12763  fsuppmapnn0fiub  12830  mulexp  12939  expadd  12942  expmul  12945  leexp1a  12959  expnbnd  13033  bccl  13149  hashdom  13206  prsshashgt1  13236  hashfacen  13276  brfi1uzind  13318  wrdnval  13367  swrdccat3blem  13541  revccat  13561  2shfti  13864  rexico  14137  cau3lem  14138  subcn2  14369  caucvgb  14454  iseraltlem1  14456  sumss  14499  fsumsplitsn  14518  incexclem  14612  supcvg  14632  mertenslem2  14661  fprodn0  14753  fprodsplitsn  14764  fprodle  14771  eftlcl  14881  reeftlcl  14882  rpnnen2lem6  14992  dvdsext  15090  3dvds  15099  3dvdsOLD  15100  sqoddm1div8z  15125  gcdcllem3  15270  bezoutr1  15329  seq1st  15331  dvdslcm  15358  lcmeq0  15360  lcmcl  15361  lcmneg  15363  lcmdvds  15368  coprmgcdb  15409  dvdsprime  15447  pc2dvds  15630  prmpwdvds  15655  unbenlem  15659  infpnlem1  15661  1arith  15678  vdwmc2  15730  ramcl  15780  mrcuni  16328  isacs1i  16365  acsfn  16367  funcpropd  16607  natpropd  16683  curfcl  16919  curf2ndf  16934  resmhm  17406  resmhm2b  17408  mhmco  17409  mhmima  17410  pwsdiagmhm  17416  gsumwsubmcl  17422  gsumwspan  17430  dfgrp2  17494  grpissubg  17661  subgint  17665  ghmmhmb  17718  resghm  17723  cntzmhm  17817  symgextf1lem  17886  f1omvdconj  17912  pmtr3ncom  17941  dfod2  18027  gexdvds  18045  subgpgp  18058  sylow1lem3  18061  frgpnabllem1  18322  dprdfeq0  18467  isdrng2  18805  cntzsubr  18860  islmodd  18917  lsslss  19009  reslmhm2b  19102  psrbaglefi  19420  mptcoe1fsupp  19633  ply1coe  19714  psgnfix1  19992  psgndif  19996  zrhcopsgndif  19997  ocvocv  20063  frlmsslsp  20183  frlmlbs  20184  mamudi  20257  mamudir  20258  mat1dimelbas  20325  scmatmulcl  20372  scmatfo  20384  mulmarep1gsum2  20428  mdetunilem7  20472  mdetunilem9  20474  gsummatr01lem3  20511  smadiadetlem3  20522  mp2pm2mplem4  20662  chfacfisf  20707  chfacfisfcpmat  20708  cpmadugsumlemF  20729  elcls  20925  leordtval  21065  cnpnei  21116  cnco  21118  cnss1  21128  cmpsub  21251  hauscmplem  21257  dissnlocfin  21380  ptbasid  21426  tx2cn  21461  upxp  21474  txindis  21485  xkoptsub  21505  xkopt  21506  trfbas2  21694  filconn  21734  trfil2  21738  filssufilg  21762  ufileu  21770  fixufil  21773  ufilen  21781  rnelfmlem  21803  flimclsi  21829  hauspwpwf1  21838  fclsopn  21865  fclsfnflim  21878  fclscmpi  21880  alexsubALTlem3  21900  alexsubALTlem4  21901  ptcmplem5  21907  tgpmulg  21944  subgtgp  21956  tgpt0  21969  tsmsxplem2  22004  metss  22360  metustfbas  22409  dscopn  22425  xrsmopn  22662  cncfss  22749  icoopnst  22785  iccpnfcnv  22790  icccvx  22796  evth  22805  phtpycc  22837  pcohtpylem  22865  lmmbrf  23106  fgcfil  23115  caucfil  23127  cfilres  23140  bcth3  23174  ovolfioo  23282  ovolficc  23283  voliunlem3  23366  volcn  23420  mbflimsup  23478  mbfi1fseqlem5  23531  itg2seq  23554  dvnff  23731  dvnadd  23737  cpnord  23743  c1liplem1  23804  plypf1  24013  plyaddlem1  24014  plymullem1  24015  coeeulem  24025  coeidlem  24038  dgrle  24044  dgrnznn  24048  plycjlem  24077  elqaalem3  24121  ulmcaulem  24193  ulmcau  24194  psergf  24211  psercn2  24222  efopn  24449  abscxpbnd  24539  leibpi  24714  isppw2  24886  muinv  24964  bposlem3  25056  gausslemma2dlem4  25139  pntrmax  25298  pntpbnd1  25320  qabvexp  25360  eqeelen  25829  colinearalglem4  25834  axcgrid  25841  axsegconlem1  25842  axsegconlem3  25844  ax5seglem1  25853  ax5seglem2  25854  ax5seglem9  25862  axcontlem2  25890  cusgrfilem2  26408  vtxdgfisf  26428  usgr2pthlem  26715  uspgrn2crct  26756  crctcshwlkn0  26769  wwlksnextproplem3  26874  eupth2lem3lem4  27209  frgr3vlem1  27253  frgr3vlem2  27254  3vfriswmgrlem  27257  frgrwopreglem5  27301  extwwlkfablem1OLD  27323  numclwwlk3lemOLD  27369  numclwwlk3lem  27371  grpoidinvlem3  27488  grpoidinv  27490  grpoideu  27491  nmoub3i  27756  nmlno0lem  27776  nmlnoubi  27779  ipasslem3  27816  ipblnfi  27839  hvaddsub4  28063  his35  28073  shsel3  28302  chj4  28522  spansncol  28555  chscllem2  28625  5oalem2  28642  3oalem2  28650  hoaddcl  28745  adjsym  28820  cnvadj  28879  hhcno  28891  hhcnf  28892  nmopub2tALT  28896  unoplin  28907  counop  28908  nmfnleub2  28913  hmoplin  28929  brafnmul  28938  nmlnop0iALT  28982  nmopun  29001  nmophmi  29018  riesz3i  29049  riesz1  29052  cnlnadjlem2  29055  cnlnadjlem6  29059  adjmul  29079  adjadd  29080  bra11  29095  cnvbraval  29097  kbass5  29107  kbass6  29108  leop2  29111  leopadd  29119  leopmuli  29120  leoptri  29123  leopnmid  29125  nmopleid  29126  pj3si  29194  hstel2  29206  cvcon3  29271  dmdmd  29287  dmdbr5  29295  mdsl0  29297  mdslmd1lem1  29312  mdslmd1lem2  29313  mdslmd3i  29319  superpos  29341  chirredlem2  29378  chirredlem3  29379  mdsymlem3  29392  mdsymlem5  29394  mdsymlem6  29395  sumdmdlem  29405  cdjreui  29419  cdj1i  29420  cdj3i  29428  foresf1o  29469  abfmpel  29583  fcomptf  29586  fcnvgreu  29600  xrge0infss  29653  cmpcref  30045  xrge0iifcnv  30107  esumcst  30253  hasheuni  30275  esum2dlem  30282  esum2d  30283  sigaclcu2  30311  insiga  30328  unelldsys  30349  measres  30413  measdivcst  30416  volfiniune  30421  ddemeas  30427  sgn3da  30731  actfunsnf1o  30810  sconnpi1  31347  cvmsss2  31382  mrsubco  31544  dfon2lem6  31817  dftrpred3g  31857  poseq  31878  soseq  31879  hfext  32415  elicc3  32436  fnessref  32477  fin2solem  33525  fin2so  33526  lindsenlbs  33534  matunitlindflem1  33535  matunitlindflem2  33536  poimirlem2  33541  poimirlem14  33553  poimirlem25  33564  poimirlem26  33565  poimirlem29  33568  poimirlem30  33569  broucube  33573  heicant  33574  mblfinlem2  33577  mblfinlem3  33578  mblfinlem4  33579  ex-ovoliunnfl  33582  mbfresfi  33586  cnambfre  33588  itg2addnclem  33591  itg2addnclem2  33592  itg2addnc  33594  bddiblnc  33610  ftc1anclem3  33617  ftc1anclem4  33618  ftc1anclem5  33619  ftc1anclem6  33620  ftc1anclem7  33621  ftc1anclem8  33622  ftc1anc  33623  eqfnun  33646  indexdom  33659  filbcmb  33665  fdc  33671  incsequz  33674  metf1o  33681  caures  33686  bndss  33715  ismtycnv  33731  heiborlem1  33740  rrncmslem  33761  isdrngo2  33887  rngoisocnv  33910  unichnidl  33960  ax12eq  34545  ax12el  34546  lshpset2N  34724  pmapglb2N  35375  pmapglb2xN  35376  pclfinN  35504  polval2N  35510  cdleme31fv2  35998  cdleme32fvcl  36045  cdleme48gfv  36142  tendoicl  36401  tendoipl  36402  diaglbN  36661  dochkr1  37084  dochkr1OLDN  37085  nacsfix  37592  eq0rabdioph  37657  diophren  37694  rencldnfilem  37701  pell1234qrdich  37742  jm2.24  37847  jm2.26lem3  37885  wepwsolem  37929  pwssplit4  37976  isnumbasgrplem3  37992  cvgdvgrat  38829  ofsubid  38840  bcc0  38856  binomcxplemnn0  38865  uzwo4  39535  fiiuncl  39548  iunincfi  39586  nsstr  39587  rexanuz3  39589  iinssiin  39626  ralimda  39640  disjrnmpt2  39689  fompt  39693  disjinfi  39694  mapsnd  39702  choicefi  39706  fsneq  39712  difmap  39713  iunmapsn  39723  axccdom  39730  axccd  39743  rnmptlb  39767  rnmptbd2lem  39777  ssfiunibd  39837  supxrgelem  39866  suplesup  39868  xrlexaddrp  39881  xralrple2  39883  infxrunb2  39897  xralrple3  39903  xrralrecnnle  39915  xrralrecnnge  39926  supxrunb3  39936  unb2ltle  39955  rexabslelem  39958  supminfrnmpt  39985  infxrpnf  39987  supminfxr  40007  supminfxr2  40012  xrpnf  40029  iooiinicc  40087  ressioosup  40100  iooiinioc  40101  ressiooinf  40102  fsumsupp0  40128  divcnvg  40177  limcrecl  40179  sumnnodd  40180  islpcn  40189  lptre2pt  40190  limcresiooub  40192  limcresioolb  40193  limclner  40201  fnlimfvre  40224  allbutfifvre  40225  climinf3  40266  limsupmnflem  40270  limsupre3uzlem  40285  limsupreuzmpt  40289  climuzlem  40293  climisp  40296  climrescn  40298  climxrrelem  40299  climxrre  40300  climlimsupcex  40319  liminflelimsuplem  40325  limsupgtlem  40327  liminfvalxr  40333  liminfreuzlem  40352  liminfltlem  40354  liminflimsupclim  40357  cnrefiisplem  40373  xlimmnfvlem2  40377  xlimmnfv  40378  xlimpnfvlem2  40381  xlimpnfv  40382  xlimmnfmpt  40387  xlimpnfmpt  40388  climxlim2lem  40389  dfxlim2v  40391  cncfuni  40417  icccncfext  40418  cncficcgt0  40419  cncfiooicclem1  40424  cncfiooiccre  40426  dvasinbx  40453  dvdsn1add  40472  dvnmul  40476  dvmptfprodlem  40477  dvnprodlem1  40479  dvnprodlem3  40481  iblspltprt  40507  itgioocnicc  40511  itgspltprt  40513  ismbl3  40521  stirlinglem5  40613  dirker2re  40627  dirkerper  40631  dirkertrigeq  40636  dirkercncflem2  40639  fourierdlem12  40654  fourierdlem15  40657  fourierdlem16  40658  fourierdlem20  40662  fourierdlem21  40663  fourierdlem22  40664  fourierdlem39  40681  fourierdlem40  40682  fourierdlem41  40683  fourierdlem42  40684  fourierdlem46  40687  fourierdlem49  40690  fourierdlem50  40691  fourierdlem57  40698  fourierdlem58  40699  fourierdlem59  40700  fourierdlem64  40705  fourierdlem65  40706  fourierdlem66  40707  fourierdlem68  40709  fourierdlem70  40711  fourierdlem71  40712  fourierdlem73  40714  fourierdlem78  40719  fourierdlem79  40720  fourierdlem80  40721  fourierdlem81  40722  fourierdlem82  40723  fourierdlem83  40724  fourierdlem87  40728  fourierdlem93  40734  fourierdlem95  40736  fourierdlem101  40742  fourierdlem103  40744  fourierdlem104  40745  fourierdlem111  40752  fourierdlem112  40753  sqwvfoura  40763  fourierswlem  40765  elaa2lem  40768  etransclem13  40782  etransclem23  40792  etransclem24  40793  etransclem32  40801  etransclem38  40807  etransclem46  40815  qndenserrnbllem  40832  rrxsnicc  40838  ioorrnopnlem  40842  prsal  40856  intsal  40866  salexct  40870  dfsalgen2  40877  issalnnd  40881  sge0rnre  40899  sge0val  40901  sge0z  40910  sge0revalmpt  40913  sge0tsms  40915  sge0pr  40929  sge0resplit  40941  sge0split  40944  sge0splitmpt  40946  sge0iunmptlemfi  40948  sge0iunmptlemre  40950  sge0fodjrnlem  40951  sge0iunmpt  40953  sge0rpcpnf  40956  sge0ltfirpmpt2  40961  sge0isum  40962  sge0xaddlem1  40968  sge0xaddlem2  40969  sge0pnffsumgt  40977  sge0gtfsumgt  40978  sge0seq  40981  sge0reuz  40982  nnfoctbdjlem  40990  nnfoctbdj  40991  meadjun  40997  meadjiunlem  41000  voliunsge0lem  41007  meaiuninc3v  41019  omeiunltfirp  41054  carageniuncllem2  41057  caratheodorylem1  41061  caratheodorylem2  41062  caratheodory  41063  isomenndlem  41065  isomennd  41066  hoicvr  41083  volicorescl  41088  ovnsubaddlem2  41106  hoidmvlelem2  41131  hoidmvlelem3  41132  hoidmvle  41135  ovnhoilem2  41137  hspdifhsp  41151  hoiqssbllem2  41158  hoiqssbllem3  41159  hspmbllem2  41162  ovnsubadd2lem  41180  ovolval4lem1  41184  vonvolmbl  41196  vonioo  41217  vonicc  41220  pimrecltpos  41240  issmfle  41275  smflimlem1  41300  smflimlem2  41301  smflimlem6  41305  smfresal  41316  smfrec  41317  smfmullem4  41322  smfpimcc  41335  smflimmpt  41337  smfsuplem1  41338  smfsuplem3  41340  smfsupmpt  41342  smfsupxr  41343  smfinflem  41344  smfinfmpt  41346  smflimsuplem4  41350  smflimsuplem5  41351  smflimsupmpt  41356  smfliminfmpt  41359  smonoord  41666  lswn0  41705  fmtnoprmfac1  41802  fmtnofac2lem  41805  sbgoldbst  41991  resmgmhm  42123  resmgmhm2b  42125  mgmhmco  42126  mgmhmima  42127  snlindsntorlem  42584  aacllem  42875
  Copyright terms: Public domain W3C validator