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

Theorem adantll 749
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 477 . 2 ((𝜃𝜑) → 𝜑)
2 adant2.1 . 2 ((𝜑𝜓) → 𝜒)
31, 2sylan 488 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 197  df-an 386
This theorem is referenced by:  ad2antlr  762  ad2ant2l  781  ad2ant2lr  783  3ad2antl3  1223  3adant1l  1315  ralcom2  3098  reu6  3382  sbc2iegf  3491  sbcralt  3497  pofun  5021  poinxp  5153  xpdifid  5531  sossfld  5549  predpo  5667  preddowncl  5676  tz7.7  5718  onfr  5732  ssimaex  6230  fndmdif  6287  dffo4  6341  foco2OLD  6346  fcompt  6365  fconst2g  6433  f1cofveqaeq  6480  2f1fvneq  6482  isores3  6550  fvmptopab  6662  limsssuc  7012  el2mpt2cl  7211  curry1  7229  curry2  7232  extmptsuppeq  7279  suppss  7285  suppssov1  7287  suppss2  7289  suppssfv  7291  onnseq  7401  oe0  7562  oesuclem  7565  oecl  7577  oaordi  7586  oawordri  7590  oaass  7601  omordi  7606  omword2  7614  omlimcl  7618  odi  7619  omass  7620  oeoe  7639  nnaordi  7658  oaabs  7684  omsmolem  7693  eceqoveq  7813  dom2lem  7955  sbthlem9  8038  php3  8106  onomeneq  8110  isinf  8133  frfi  8165  fiint  8197  fodomfib  8200  fofinf1o  8201  marypha1lem  8299  ordiso2  8380  unwdomg  8449  xpwdomg  8450  ac5num  8819  cff1  9040  cfcoflem  9054  infpssrlem4  9088  isf32lem9  9143  isf34lem7  9161  fin1a2lem13  9194  fin1a2s  9196  hsmexlem4  9211  axdc2lem  9230  zorn2lem6  9283  axpowndlem2  9380  inttsk  9556  tskuni  9565  nqereu  9711  prcdnq  9775  addclprlem2  9799  ltexpri  9825  prlem936  9829  reclem2pr  9830  axsup  10073  add4  10216  ltleadd  10471  lt2mul2div  10861  lediv12a  10876  nn2ge  11005  zextle  11410  fnn0ind  11436  xrlttr  11933  ifle  11987  xaddass  12038  xmulasslem3  12075  xlemul1a  12077  xadddilem  12083  xrsupsslem  12096  xrinfmsslem  12097  supxrunb1  12108  supxrunb2  12109  ixxin  12150  difreicc  12262  iccsplit  12263  iccshftr  12264  iccshftl  12266  iccdil  12268  icccntr  12270  fzaddel  12333  fzadd2  12334  fzrev  12361  modadd1  12663  modmul1  12679  fsuppmapnn0fiub  12746  mulexp  12855  expadd  12858  expmul  12861  leexp1a  12875  expnbnd  12949  bccl  13065  hashdom  13124  prsshashgt1  13154  hashfacen  13192  brfi1uzind  13235  brfi1uzindOLD  13241  wrdnval  13290  swrdccat3blem  13448  revccat  13468  2shfti  13770  rexico  14043  cau3lem  14044  subcn2  14275  caucvgb  14360  iseraltlem1  14362  sumss  14404  fsumsplitsn  14423  incexclem  14512  supcvg  14532  mertenslem2  14561  fprodn0  14653  fprodsplitsn  14664  fprodle  14671  eftlcl  14781  reeftlcl  14782  rpnnen2lem6  14892  dvdsext  14986  3dvds  14995  3dvdsOLD  14996  sqoddm1div8z  15021  gcdcllem3  15166  bezoutr1  15225  seq1st  15227  dvdslcm  15254  lcmeq0  15256  lcmcl  15257  lcmneg  15259  lcmdvds  15264  coprmgcdb  15305  dvdsprime  15343  pc2dvds  15526  prmpwdvds  15551  unbenlem  15555  infpnlem1  15557  1arith  15574  vdwmc2  15626  ramcl  15676  mrcuni  16221  isacs1i  16258  acsfn  16260  funcpropd  16500  natpropd  16576  curfcl  16812  curf2ndf  16827  resmhm  17299  resmhm2b  17301  mhmco  17302  mhmima  17303  pwsdiagmhm  17309  gsumwsubmcl  17315  gsumwspan  17323  dfgrp2  17387  grpissubg  17554  subgint  17558  ghmmhmb  17611  resghm  17616  cntzmhm  17711  symgextf1lem  17780  f1omvdconj  17806  pmtr3ncom  17835  dfod2  17921  gexdvds  17939  subgpgp  17952  sylow1lem3  17955  frgpnabllem1  18216  dprdfeq0  18361  isdrng2  18697  cntzsubr  18752  islmodd  18809  lsslss  18901  reslmhm2b  18994  psrbaglefi  19312  mptcoe1fsupp  19525  ply1coe  19606  psgnfix1  19884  psgndif  19888  zrhcopsgndif  19889  ocvocv  19955  frlmsslsp  20075  frlmlbs  20076  mamudi  20149  mamudir  20150  mat1dimelbas  20217  scmatmulcl  20264  scmatfo  20276  mulmarep1gsum2  20320  mdetunilem7  20364  mdetunilem9  20366  gsummatr01lem3  20403  smadiadetlem3  20414  mp2pm2mplem4  20554  chfacfisf  20599  chfacfisfcpmat  20600  cpmadugsumlemF  20621  elcls  20817  leordtval  20957  cnpnei  21008  cnco  21010  cnss1  21020  cmpsub  21143  hauscmplem  21149  dissnlocfin  21272  ptbasid  21318  tx2cn  21353  upxp  21366  txindis  21377  xkoptsub  21397  xkopt  21398  trfbas2  21587  filconn  21627  trfil2  21631  filssufilg  21655  ufileu  21663  fixufil  21666  ufilen  21674  rnelfmlem  21696  flimclsi  21722  hauspwpwf1  21731  fclsopn  21758  fclsfnflim  21771  fclscmpi  21773  alexsubALTlem3  21793  alexsubALTlem4  21794  ptcmplem5  21800  tgpmulg  21837  subgtgp  21849  tgpt0  21862  tsmsxplem2  21897  metss  22253  metustfbas  22302  dscopn  22318  xrsmopn  22555  cncfss  22642  icoopnst  22678  iccpnfcnv  22683  icccvx  22689  evth  22698  phtpycc  22730  pcohtpylem  22759  lmmbrf  23000  fgcfil  23009  caucfil  23021  cfilres  23034  bcth3  23068  ovolfioo  23176  ovolficc  23177  voliunlem3  23260  volcn  23314  mbflimsup  23373  mbfi1fseqlem5  23426  itg2seq  23449  dvnff  23626  dvnadd  23632  cpnord  23638  c1liplem1  23697  plypf1  23906  plyaddlem1  23907  plymullem1  23908  coeeulem  23918  coeidlem  23931  dgrle  23937  dgrnznn  23941  plycjlem  23970  elqaalem3  24014  ulmcaulem  24086  ulmcau  24087  psergf  24104  psercn2  24115  efopn  24338  abscxpbnd  24428  leibpi  24603  isppw2  24775  muinv  24853  bposlem3  24945  gausslemma2dlem4  25028  pntrmax  25187  pntpbnd1  25209  qabvexp  25249  eqeelen  25718  colinearalglem4  25723  axcgrid  25730  axsegconlem1  25731  axsegconlem3  25733  ax5seglem1  25742  ax5seglem2  25743  ax5seglem9  25751  axcontlem2  25779  egrsubgr  26096  cusgrfilem2  26273  vtxdgfisf  26292  usgr2pthlem  26562  uspgrn2crct  26603  crctcshwlkn0  26616  wwlksnextproplem3  26709  eupth2lem3lem4  26991  frgr3vlem1  27035  frgr3vlem2  27036  3vfriswmgrlem  27039  frgrhash2wsp  27089  extwwlkfablem2  27102  numclwwlkovf2ex  27109  numclwwlk3lem  27130  grpoidinvlem3  27248  grpoidinv  27250  grpoideu  27251  nmoub3i  27516  nmlno0lem  27536  nmlnoubi  27539  ipasslem3  27576  ipblnfi  27599  hvaddsub4  27823  his35  27833  shsel3  28062  chj4  28282  spansncol  28315  chscllem2  28385  5oalem2  28402  3oalem2  28410  hoaddcl  28505  adjsym  28580  cnvadj  28639  hhcno  28651  hhcnf  28652  nmopub2tALT  28656  unoplin  28667  counop  28668  nmfnleub2  28673  hmoplin  28689  brafnmul  28698  nmlnop0iALT  28742  nmopun  28761  nmophmi  28778  riesz3i  28809  riesz1  28812  cnlnadjlem2  28815  cnlnadjlem6  28819  adjmul  28839  adjadd  28840  bra11  28855  cnvbraval  28857  kbass5  28867  kbass6  28868  leop2  28871  leopadd  28879  leopmuli  28880  leoptri  28883  leopnmid  28885  nmopleid  28886  pj3si  28954  hstel2  28966  cvcon3  29031  dmdmd  29047  dmdbr5  29055  mdsl0  29057  mdslmd1lem1  29072  mdslmd1lem2  29073  mdslmd3i  29079  superpos  29101  chirredlem2  29138  chirredlem3  29139  mdsymlem3  29152  mdsymlem5  29154  mdsymlem6  29155  sumdmdlem  29165  cdjreui  29179  cdj1i  29180  cdj3i  29188  foresf1o  29231  abfmpel  29338  fcomptf  29341  fcnvgreu  29356  xrge0infss  29410  cmpcref  29741  xrge0iifcnv  29803  esumcst  29948  hasheuni  29970  esum2dlem  29977  esum2d  29978  sigaclcu2  30006  insiga  30023  unelldsys  30044  measres  30108  measdivcst  30111  volfiniune  30116  ddemeas  30122  sgn3da  30426  sconnpi1  30982  cvmsss2  31017  mrsubco  31179  dfon2lem6  31447  dftrpred3g  31487  poseq  31504  soseq  31505  nodenselem3  31599  nobndlem6  31613  hfext  31985  elicc3  32006  fnessref  32047  fin2solem  33066  fin2so  33067  lindsenlbs  33075  matunitlindflem1  33076  matunitlindflem2  33077  poimirlem2  33082  poimirlem14  33094  poimirlem25  33105  poimirlem26  33106  poimirlem29  33109  poimirlem30  33110  broucube  33114  heicant  33115  mblfinlem2  33118  mblfinlem3  33119  mblfinlem4  33120  ex-ovoliunnfl  33123  mbfresfi  33127  cnambfre  33129  itg2addnclem  33132  itg2addnclem2  33133  itg2addnc  33135  bddiblnc  33151  ftc1anclem3  33158  ftc1anclem4  33159  ftc1anclem5  33160  ftc1anclem6  33161  ftc1anclem7  33162  ftc1anclem8  33163  ftc1anc  33164  eqfnun  33187  indexdom  33200  filbcmb  33206  fdc  33212  incsequz  33215  metf1o  33222  caures  33227  bndss  33256  ismtycnv  33272  heiborlem1  33281  rrncmslem  33302  isdrngo2  33428  rngoisocnv  33451  unichnidl  33501  ax12eq  33745  ax12el  33746  lshpset2N  33925  pmapglb2N  34576  pmapglb2xN  34577  pclfinN  34705  polval2N  34711  cdleme31fv2  35200  cdleme32fvcl  35247  cdleme48gfv  35344  tendoicl  35603  tendoipl  35604  diaglbN  35863  dochkr1  36286  dochkr1OLDN  36287  nacsfix  36794  eq0rabdioph  36859  diophren  36896  rencldnfilem  36903  pell1234qrdich  36944  jm2.24  37049  jm2.26lem3  37087  wepwsolem  37131  pwssplit4  37178  isnumbasgrplem3  37195  cvgdvgrat  38033  ofsubid  38044  bcc0  38060  binomcxplemnn0  38069  uzwo4  38743  fiiuncl  38756  iunincfi  38794  nsstr  38795  rexanuz3  38797  iinssiin  38837  ralimda  38852  disjrnmpt2  38884  fompt  38888  disjinfi  38889  mapsnd  38897  choicefi  38901  fsneq  38907  difmap  38908  iunmapsn  38918  axccdom  38925  axccd  38938  rnmptlb  38963  rnmptbd2lem  38974  ssfiunibd  39022  supxrgelem  39052  suplesup  39054  xrlexaddrp  39067  xralrple2  39069  infxrunb2  39083  xralrple3  39089  xrralrecnnle  39101  xrralrecnnge  39112  supxrunb3  39122  unb2ltle  39141  rexabslelem  39144  iooiinicc  39215  ressioosup  39228  iooiinioc  39229  ressiooinf  39230  fsumsupp0  39246  divcnvg  39295  limcrecl  39297  sumnnodd  39298  islpcn  39307  lptre2pt  39308  limcresiooub  39310  limcresioolb  39311  limclner  39319  fnlimfvre  39342  allbutfifvre  39343  climinf3  39384  limsupmnflem  39388  limsupre3uzlem  39403  limsupreuzmpt  39407  cncfuni  39434  icccncfext  39435  cncficcgt0  39436  cncfiooicclem1  39441  cncfiooiccre  39443  dvasinbx  39472  dvdsn1add  39491  dvnmul  39495  dvmptfprodlem  39496  dvnprodlem1  39498  dvnprodlem3  39500  iblspltprt  39526  itgioocnicc  39530  itgspltprt  39532  ismbl3  39540  stirlinglem5  39632  dirker2re  39646  dirkerper  39650  dirkertrigeq  39655  dirkercncflem2  39658  fourierdlem12  39673  fourierdlem15  39676  fourierdlem16  39677  fourierdlem20  39681  fourierdlem21  39682  fourierdlem22  39683  fourierdlem39  39700  fourierdlem40  39701  fourierdlem41  39702  fourierdlem42  39703  fourierdlem46  39706  fourierdlem49  39709  fourierdlem50  39710  fourierdlem57  39717  fourierdlem58  39718  fourierdlem59  39719  fourierdlem64  39724  fourierdlem65  39725  fourierdlem66  39726  fourierdlem68  39728  fourierdlem70  39730  fourierdlem71  39731  fourierdlem73  39733  fourierdlem78  39738  fourierdlem79  39739  fourierdlem80  39740  fourierdlem81  39741  fourierdlem82  39742  fourierdlem83  39743  fourierdlem87  39747  fourierdlem93  39753  fourierdlem95  39755  fourierdlem101  39761  fourierdlem103  39763  fourierdlem104  39764  fourierdlem111  39771  fourierdlem112  39772  sqwvfoura  39782  fourierswlem  39784  elaa2lem  39787  etransclem13  39801  etransclem23  39811  etransclem24  39812  etransclem32  39820  etransclem38  39826  etransclem46  39834  qndenserrnbllem  39851  rrxsnicc  39857  ioorrnopnlem  39861  prsal  39875  intsal  39885  salexct  39889  dfsalgen2  39896  issalnnd  39900  sge0rnre  39918  sge0val  39920  sge0z  39929  sge0revalmpt  39932  sge0tsms  39934  sge0pr  39948  sge0resplit  39960  sge0split  39963  sge0splitmpt  39965  sge0iunmptlemfi  39967  sge0iunmptlemre  39969  sge0fodjrnlem  39970  sge0iunmpt  39972  sge0rpcpnf  39975  sge0ltfirpmpt2  39980  sge0isum  39981  sge0xaddlem1  39987  sge0xaddlem2  39988  sge0pnffsumgt  39996  sge0gtfsumgt  39997  sge0seq  40000  sge0reuz  40001  nnfoctbdjlem  40009  nnfoctbdj  40010  meadjun  40016  meadjiunlem  40019  voliunsge0lem  40026  omeiunltfirp  40070  carageniuncllem2  40073  caratheodorylem1  40077  caratheodorylem2  40078  caratheodory  40079  isomenndlem  40081  isomennd  40082  hoicvr  40099  volicorescl  40104  ovnsubaddlem2  40122  hoidmvlelem2  40147  hoidmvlelem3  40148  hoidmvle  40151  ovnhoilem2  40153  hspdifhsp  40167  hoiqssbllem2  40174  hoiqssbllem3  40175  hspmbllem2  40178  ovnsubadd2lem  40196  ovolval4lem1  40200  vonvolmbl  40212  vonioo  40233  vonicc  40236  pimrecltpos  40256  issmfle  40291  smflimlem1  40316  smflimlem2  40317  smflimlem6  40321  smfresal  40332  smfrec  40333  smfmullem4  40338  smfpimcc  40351  smflimmpt  40353  smfsuplem1  40354  smfsuplem3  40356  smfsupmpt  40358  smfsupxr  40359  smfinflem  40360  smfinfmpt  40362  smflimsuplem4  40366  smflimsuplem5  40367  smflimsupmpt  40372  smonoord  40669  lswn0  40708  fmtnoprmfac1  40806  fmtnofac2lem  40809  bgoldbst  40991  resmgmhm  41116  resmgmhm2b  41118  mgmhmco  41119  mgmhmima  41120  snlindsntorlem  41577  aacllem  41880
  Copyright terms: Public domain W3C validator