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

Theorem adantll 745
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 475 . 2 ((𝜃𝜑) → 𝜑)
2 adant2.1 . 2 ((𝜑𝜓) → 𝜒)
31, 2sylan 486 1 (((𝜃𝜑) ∧ 𝜓) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 195  df-an 384
This theorem is referenced by:  ad2antlr  758  ad2ant2l  777  ad2ant2lr  779  3ad2antl3  1217  3adant1l  1309  ralcom2  3082  reu6  3361  sbc2iegf  3470  sbcralt  3476  pofun  4965  poinxp  5095  xpdifid  5467  sossfld  5485  predpo  5601  preddowncl  5610  tz7.7  5652  onfr  5666  ssimaex  6158  fndmdif  6214  dffo4  6268  foco2OLD  6273  fcompt  6291  fconst2g  6351  isores3  6463  limsssuc  6919  el2mpt2cl  7115  curry1  7133  curry2  7136  extmptsuppeq  7183  suppss  7189  suppssov1  7191  suppss2  7193  suppssfv  7195  onnseq  7305  oe0  7466  oesuclem  7469  oecl  7481  oaordi  7490  oawordri  7494  oaass  7505  omordi  7510  omword2  7518  omlimcl  7522  odi  7523  omass  7524  oeoe  7543  nnaordi  7562  oaabs  7588  omsmolem  7597  eceqoveq  7717  dom2lem  7858  sbthlem9  7940  php3  8008  onomeneq  8012  isinf  8035  frfi  8067  fiint  8099  fodomfib  8102  fofinf1o  8103  marypha1lem  8199  ordiso2  8280  unwdomg  8349  xpwdomg  8350  ac5num  8719  cff1  8940  cfcoflem  8954  infpssrlem4  8988  isf32lem9  9043  isf34lem7  9061  fin1a2lem13  9094  fin1a2s  9096  hsmexlem4  9111  axdc2lem  9130  zorn2lem6  9183  axpowndlem2  9276  inttsk  9452  tskuni  9461  nqereu  9607  prcdnq  9671  addclprlem2  9695  ltexpri  9721  prlem936  9725  reclem2pr  9726  axsup  9964  add4  10107  ltleadd  10360  lt2mul2div  10750  lediv12a  10765  nn2ge  10892  zextle  11282  fnn0ind  11308  xrlttr  11808  ifle  11861  xaddass  11908  xmulasslem3  11945  xlemul1a  11947  xadddilem  11953  xrsupsslem  11965  xrinfmsslem  11966  supxrunb1  11977  supxrunb2  11978  ixxin  12019  difreicc  12131  iccsplit  12132  iccshftr  12133  iccshftl  12135  iccdil  12137  icccntr  12139  fzaddel  12201  fzadd2  12202  fzrev  12228  modadd1  12524  modmul1  12540  fsuppmapnn0fiub  12607  mulexp  12716  expadd  12719  expmul  12722  leexp1a  12736  expnbnd  12810  bccl  12926  hashdom  12981  prsshashgt1  13011  hashfacen  13047  brfi1uzind  13081  brfi1uzindOLD  13087  wrdnval  13136  swrdccat3blem  13292  revccat  13312  2shfti  13614  rexico  13887  cau3lem  13888  subcn2  14119  caucvgb  14204  iseraltlem1  14206  sumss  14248  incexclem  14353  supcvg  14373  mertenslem2  14402  fprodn0  14494  fprodsplitsn  14505  fprodle  14512  eftlcl  14622  reeftlcl  14623  rpnnen2lem6  14733  dvdsext  14827  3dvds  14836  3dvdsOLD  14837  sqoddm1div8z  14862  gcdcllem3  15007  bezoutr1  15066  seq1st  15068  dvdslcm  15095  lcmeq0  15097  lcmcl  15098  lcmneg  15100  lcmdvds  15105  coprmgcdb  15146  dvdsprime  15184  pc2dvds  15367  prmpwdvds  15392  unbenlem  15396  infpnlem1  15398  1arith  15415  vdwmc2  15467  ramcl  15517  mrcuni  16050  isacs1i  16087  acsfn  16089  funcpropd  16329  natpropd  16405  curfcl  16641  curf2ndf  16656  resmhm  17128  resmhm2b  17130  mhmco  17131  mhmima  17132  pwsdiagmhm  17138  gsumwsubmcl  17144  gsumwspan  17152  dfgrp2  17216  grpissubg  17383  subgint  17387  ghmmhmb  17440  resghm  17445  cntzmhm  17540  symgextf1lem  17609  f1omvdconj  17635  pmtr3ncom  17664  dfod2  17750  gexdvds  17768  subgpgp  17781  sylow1lem3  17784  frgpnabllem1  18045  dprdfeq0  18190  isdrng2  18526  cntzsubr  18581  islmodd  18638  lsslss  18728  reslmhm2b  18821  psrbaglefi  19139  mptcoe1fsupp  19352  ply1coe  19433  psgnfix1  19708  psgndif  19712  zrhcopsgndif  19713  ocvocv  19776  frlmsslsp  19896  frlmlbs  19897  mamudi  19970  mamudir  19971  mat1dimelbas  20038  scmatmulcl  20085  scmatfo  20097  mulmarep1gsum2  20141  mdetunilem7  20185  mdetunilem9  20187  gsummatr01lem3  20224  smadiadetlem3  20235  mp2pm2mplem4  20375  chfacfisf  20420  chfacfisfcpmat  20421  cpmadugsumlemF  20442  elcls  20629  leordtval  20769  cnpnei  20820  cnco  20822  cnss1  20832  cmpsub  20955  hauscmplem  20961  dissnlocfin  21084  ptbasid  21130  tx2cn  21165  upxp  21178  txindis  21189  xkoptsub  21209  xkopt  21210  trfbas2  21399  filcon  21439  trfil2  21443  filssufilg  21467  ufileu  21475  fixufil  21478  ufilen  21486  rnelfmlem  21508  flimclsi  21534  hauspwpwf1  21543  fclsopn  21570  fclsfnflim  21583  fclscmpi  21585  alexsubALTlem3  21605  alexsubALTlem4  21606  ptcmplem5  21612  tgpmulg  21649  subgtgp  21661  tgpt0  21674  tsmsxplem2  21709  metss  22064  metustfbas  22113  dscopn  22129  xrsmopn  22355  cncfss  22441  icoopnst  22477  iccpnfcnv  22482  icccvx  22488  evth  22497  phtpycc  22529  pcohtpylem  22558  lmmbrf  22786  fgcfil  22795  caucfil  22807  cfilres  22820  bcth3  22853  ovolfioo  22960  ovolficc  22961  voliunlem3  23044  volcn  23097  mbflimsup  23156  mbfi1fseqlem5  23209  itg2seq  23232  dvnff  23409  dvnadd  23415  cpnord  23421  c1liplem1  23480  plypf1  23689  plyaddlem1  23690  plymullem1  23691  coeeulem  23701  coeidlem  23714  dgrle  23720  dgrnznn  23724  plycjlem  23753  elqaalem3  23797  ulmcaulem  23869  ulmcau  23870  psergf  23887  psercn2  23898  efopn  24121  abscxpbnd  24211  leibpi  24386  isppw2  24558  muinv  24636  bposlem3  24728  gausslemma2dlem4  24811  pntrmax  24970  pntpbnd1  24992  qabvexp  25032  eqeelen  25502  colinearalglem4  25507  axcgrid  25514  axsegconlem1  25515  axsegconlem3  25517  ax5seglem1  25526  ax5seglem2  25527  ax5seglem9  25535  axcontlem2  25563  usgraidx2vlem2  25687  cusgrares  25767  cusgrafilem2  25774  wlkiswwlk1  25984  wwlkextproplem3  26037  el2wlkonot  26162  el2spthonot0  26164  usgravd00  26212  rusgraprop4  26237  eupath2lem3  26272  frgrancvvdeqlemB  26331  frgrawopreglem5  26341  frghash2spot  26356  numclwwlkun  26372  numclwwlkovf2ex  26379  grpoidinvlem3  26510  grpoidinv  26512  grpoideu  26513  nmoub3i  26818  nmlno0lem  26838  nmlnoubi  26841  ipasslem3  26878  ipblnfi  26901  hvaddsub4  27125  his35  27135  shsel3  27364  chj4  27584  spansncol  27617  chscllem2  27687  5oalem2  27704  3oalem2  27712  hoaddcl  27807  adjsym  27882  cnvadj  27941  hhcno  27953  hhcnf  27954  nmopub2tALT  27958  unoplin  27969  counop  27970  nmfnleub2  27975  hmoplin  27991  brafnmul  28000  nmlnop0iALT  28044  nmopun  28063  nmophmi  28080  riesz3i  28111  riesz1  28114  cnlnadjlem2  28117  cnlnadjlem6  28121  adjmul  28141  adjadd  28142  bra11  28157  cnvbraval  28159  kbass5  28169  kbass6  28170  leop2  28173  leopadd  28181  leopmuli  28182  leoptri  28185  leopnmid  28187  nmopleid  28188  pj3si  28256  hstel2  28268  cvcon3  28333  dmdmd  28349  dmdbr5  28357  mdsl0  28359  mdslmd1lem1  28374  mdslmd1lem2  28375  mdslmd3i  28381  superpos  28403  chirredlem2  28440  chirredlem3  28441  mdsymlem3  28454  mdsymlem5  28456  mdsymlem6  28457  sumdmdlem  28467  cdjreui  28481  cdj1i  28482  cdj3i  28490  foresf1o  28533  abfmpel  28641  fcomptf  28646  fcnvgreu  28661  xrge0infss  28721  cmpcref  29051  xrge0iifcnv  29113  esumcst  29258  hasheuni  29280  esum2dlem  29287  esum2d  29288  sigaclcu2  29316  insiga  29333  unelldsys  29354  measres  29418  measdivcst  29421  volfiniune  29426  ddemeas  29432  sgn3da  29736  sconpi1  30281  cvmsss2  30316  mrsubco  30478  dfon2lem6  30743  dftrpred3g  30783  poseq  30800  soseq  30801  nodenselem3  30888  nobndlem6  30902  hfext  31266  elicc3  31287  fnessref  31328  fin2solem  32361  fin2so  32362  lindsenlbs  32370  matunitlindflem1  32371  matunitlindflem2  32372  poimirlem2  32377  poimirlem14  32389  poimirlem25  32400  poimirlem26  32401  poimirlem29  32404  poimirlem30  32405  broucube  32409  heicant  32410  mblfinlem2  32413  mblfinlem3  32414  mblfinlem4  32415  ex-ovoliunnfl  32418  mbfresfi  32422  cnambfre  32424  itg2addnclem  32427  itg2addnclem2  32428  itg2addnc  32430  bddiblnc  32446  ftc1anclem3  32453  ftc1anclem4  32454  ftc1anclem5  32455  ftc1anclem6  32456  ftc1anclem7  32457  ftc1anclem8  32458  ftc1anc  32459  eqfnun  32482  indexdom  32495  filbcmb  32501  fdc  32507  incsequz  32510  metf1o  32517  caures  32522  bndss  32551  ismtycnv  32567  heiborlem1  32576  rrncmslem  32597  isdrngo2  32723  rngoisocnv  32746  unichnidl  32796  ax12eq  33040  ax12el  33041  lshpset2N  33220  pmapglb2N  33871  pmapglb2xN  33872  pclfinN  34000  polval2N  34006  cdleme31fv2  34495  cdleme32fvcl  34542  cdleme48gfv  34639  tendoicl  34898  tendoipl  34899  diaglbN  35158  dochkr1  35581  dochkr1OLDN  35582  nacsfix  36089  eq0rabdioph  36154  diophren  36191  rencldnfilem  36198  pell1234qrdich  36239  jm2.24  36344  jm2.26lem3  36382  wepwsolem  36426  pwssplit4  36473  isnumbasgrplem3  36490  cvgdvgrat  37330  ofsubid  37341  bcc0  37357  binomcxplemnn0  37366  uzwo4  38042  fiiuncl  38055  iunincfi  38096  nsstr  38097  rexanuz3  38099  disjrnmpt2  38166  fompt  38170  disjinfi  38171  mapsnd  38179  choicefi  38183  fsneq  38189  difmap  38190  iunmapsn  38200  axccdom  38207  axccd  38220  ssfiunibd  38260  supxrgelem  38291  suplesup  38293  xrlexaddrp  38306  xralrple2  38308  infxrunb2  38322  xralrple3  38328  xrralrecnnle  38340  xrralrecnnge  38351  iooiinicc  38413  ressioosup  38426  iooiinioc  38427  ressiooinf  38428  fsumsplitsn  38434  fsumsupp0  38442  divcnvg  38491  limcrecl  38493  sumnnodd  38494  islpcn  38503  lptre2pt  38504  limcresiooub  38506  limcresioolb  38507  limclner  38515  fnlimfvre  38538  allbutfifvre  38539  cncfuni  38569  icccncfext  38570  cncficcgt0  38571  cncfiooicclem1  38576  cncfiooiccre  38578  dvasinbx  38607  dvdsn1add  38626  dvnmul  38630  dvmptfprodlem  38631  dvnprodlem1  38633  dvnprodlem3  38635  iblspltprt  38662  itgioocnicc  38666  itgspltprt  38668  ismbl3  38676  stirlinglem5  38768  dirker2re  38782  dirkerper  38786  dirkertrigeq  38791  dirkercncflem2  38794  fourierdlem12  38809  fourierdlem15  38812  fourierdlem16  38813  fourierdlem20  38817  fourierdlem21  38818  fourierdlem22  38819  fourierdlem39  38836  fourierdlem40  38837  fourierdlem41  38838  fourierdlem42  38839  fourierdlem46  38842  fourierdlem49  38845  fourierdlem50  38846  fourierdlem57  38853  fourierdlem58  38854  fourierdlem59  38855  fourierdlem64  38860  fourierdlem65  38861  fourierdlem66  38862  fourierdlem68  38864  fourierdlem70  38866  fourierdlem71  38867  fourierdlem73  38869  fourierdlem78  38874  fourierdlem79  38875  fourierdlem80  38876  fourierdlem81  38877  fourierdlem82  38878  fourierdlem83  38879  fourierdlem87  38883  fourierdlem93  38889  fourierdlem95  38891  fourierdlem101  38897  fourierdlem103  38899  fourierdlem104  38900  fourierdlem111  38907  fourierdlem112  38908  sqwvfoura  38918  fourierswlem  38920  elaa2lem  38923  etransclem13  38937  etransclem23  38947  etransclem24  38948  etransclem32  38956  etransclem38  38962  etransclem46  38970  qndenserrnbllem  38987  rrxsnicc  38993  ioorrnopnlem  38997  prsal  39011  intsal  39021  salexct  39025  dfsalgen2  39032  issalnnd  39036  sge0rnre  39054  sge0val  39056  sge0z  39065  sge0revalmpt  39068  sge0tsms  39070  sge0pr  39084  sge0resplit  39096  sge0split  39099  sge0splitmpt  39101  sge0iunmptlemfi  39103  sge0iunmptlemre  39105  sge0fodjrnlem  39106  sge0iunmpt  39108  sge0rpcpnf  39111  sge0ltfirpmpt2  39116  sge0isum  39117  sge0xaddlem1  39123  sge0xaddlem2  39124  sge0pnffsumgt  39132  sge0gtfsumgt  39133  sge0seq  39136  sge0reuz  39137  nnfoctbdjlem  39145  nnfoctbdj  39146  meadjun  39152  meadjiunlem  39155  voliunsge0lem  39162  omeiunltfirp  39206  carageniuncllem2  39209  caratheodorylem1  39213  caratheodorylem2  39214  caratheodory  39215  isomenndlem  39217  isomennd  39218  hoicvr  39235  volicorescl  39240  ovnsubaddlem2  39258  hoidmvlelem2  39283  hoidmvlelem3  39284  hoidmvle  39287  ovnhoilem2  39289  hspdifhsp  39303  hoiqssbllem2  39310  hoiqssbllem3  39311  hspmbllem2  39314  ovnsubadd2lem  39332  ovolval4lem1  39336  vonvolmbl  39348  vonioo  39370  vonicc  39373  pimrecltpos  39393  issmfle  39429  smflimlem1  39454  smflimlem2  39455  smflimlem6  39459  smfresal  39470  smfrec  39471  smfmullem4  39476  smonoord  39742  fmtnoprmfac1  39813  fmtnofac2lem  39816  bgoldbst  39998  lswn0  40040  2f1fvneq  40131  f1cofveqaeq  40132  egrsubgr  40496  cusgrfilem2  40667  vtxdgfisf  40686  usgr2pthlem  40964  uspgrn2crct  41006  crctcsh1wlkn0  41019  wwlksnextproplem3  41112  eupth2lem3lem4  41394  frgr3vlem1  41438  frgr3vlem2  41439  3vfriswmgrlem  41442  frgrhash2wsp  41492  av-extwwlkfablem2  41505  av-numclwwlkovf2ex  41512  av-numclwwlk3lem  41533  resmgmhm  41583  resmgmhm2b  41585  mgmhmco  41586  mgmhmima  41587  snlindsntorlem  42048  aacllem  42312
  Copyright terms: Public domain W3C validator