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

Theorem adantll 746
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 196  df-an 385
This theorem is referenced by:  ad2antlr  759  ad2ant2l  778  ad2ant2lr  780  3ad2antl3  1218  3adant1l  1310  ralcom2  3083  reu6  3362  sbc2iegf  3471  sbcralt  3477  pofun  4975  poinxp  5105  xpdifid  5481  sossfld  5499  predpo  5615  preddowncl  5624  tz7.7  5666  onfr  5680  ssimaex  6173  fndmdif  6229  dffo4  6283  foco2OLD  6288  fcompt  6306  fconst2g  6373  isores3  6485  limsssuc  6942  el2mpt2cl  7138  curry1  7156  curry2  7159  extmptsuppeq  7206  suppss  7212  suppssov1  7214  suppss2  7216  suppssfv  7218  onnseq  7328  oe0  7489  oesuclem  7492  oecl  7504  oaordi  7513  oawordri  7517  oaass  7528  omordi  7533  omword2  7541  omlimcl  7545  odi  7546  omass  7547  oeoe  7566  nnaordi  7585  oaabs  7611  omsmolem  7620  eceqoveq  7740  dom2lem  7881  sbthlem9  7963  php3  8031  onomeneq  8035  isinf  8058  frfi  8090  fiint  8122  fodomfib  8125  fofinf1o  8126  marypha1lem  8222  ordiso2  8303  unwdomg  8372  xpwdomg  8373  ac5num  8742  cff1  8963  cfcoflem  8977  infpssrlem4  9011  isf32lem9  9066  isf34lem7  9084  fin1a2lem13  9117  fin1a2s  9119  hsmexlem4  9134  axdc2lem  9153  zorn2lem6  9206  axpowndlem2  9299  inttsk  9475  tskuni  9484  nqereu  9630  prcdnq  9694  addclprlem2  9718  ltexpri  9744  prlem936  9748  reclem2pr  9749  axsup  9992  add4  10135  ltleadd  10390  lt2mul2div  10780  lediv12a  10795  nn2ge  10922  zextle  11326  fnn0ind  11352  xrlttr  11849  ifle  11902  xaddass  11951  xmulasslem3  11988  xlemul1a  11990  xadddilem  11996  xrsupsslem  12009  xrinfmsslem  12010  supxrunb1  12021  supxrunb2  12022  ixxin  12063  difreicc  12175  iccsplit  12176  iccshftr  12177  iccshftl  12179  iccdil  12181  icccntr  12183  fzaddel  12246  fzadd2  12247  fzrev  12273  modadd1  12569  modmul1  12585  fsuppmapnn0fiub  12652  mulexp  12761  expadd  12764  expmul  12767  leexp1a  12781  expnbnd  12855  bccl  12971  hashdom  13029  prsshashgt1  13059  hashfacen  13095  brfi1uzind  13135  brfi1uzindOLD  13141  wrdnval  13190  swrdccat3blem  13346  revccat  13366  2shfti  13668  rexico  13941  cau3lem  13942  subcn2  14173  caucvgb  14258  iseraltlem1  14260  sumss  14302  incexclem  14407  supcvg  14427  mertenslem2  14456  fprodn0  14548  fprodsplitsn  14559  fprodle  14566  eftlcl  14676  reeftlcl  14677  rpnnen2lem6  14787  dvdsext  14881  3dvds  14890  3dvdsOLD  14891  sqoddm1div8z  14916  gcdcllem3  15061  bezoutr1  15120  seq1st  15122  dvdslcm  15149  lcmeq0  15151  lcmcl  15152  lcmneg  15154  lcmdvds  15159  coprmgcdb  15200  dvdsprime  15238  pc2dvds  15421  prmpwdvds  15446  unbenlem  15450  infpnlem1  15452  1arith  15469  vdwmc2  15521  ramcl  15571  mrcuni  16104  isacs1i  16141  acsfn  16143  funcpropd  16383  natpropd  16459  curfcl  16695  curf2ndf  16710  resmhm  17182  resmhm2b  17184  mhmco  17185  mhmima  17186  pwsdiagmhm  17192  gsumwsubmcl  17198  gsumwspan  17206  dfgrp2  17270  grpissubg  17437  subgint  17441  ghmmhmb  17494  resghm  17499  cntzmhm  17594  symgextf1lem  17663  f1omvdconj  17689  pmtr3ncom  17718  dfod2  17804  gexdvds  17822  subgpgp  17835  sylow1lem3  17838  frgpnabllem1  18099  dprdfeq0  18244  isdrng2  18580  cntzsubr  18635  islmodd  18692  lsslss  18782  reslmhm2b  18875  psrbaglefi  19193  mptcoe1fsupp  19406  ply1coe  19487  psgnfix1  19763  psgndif  19767  zrhcopsgndif  19768  ocvocv  19834  frlmsslsp  19954  frlmlbs  19955  mamudi  20028  mamudir  20029  mat1dimelbas  20096  scmatmulcl  20143  scmatfo  20155  mulmarep1gsum2  20199  mdetunilem7  20243  mdetunilem9  20245  gsummatr01lem3  20282  smadiadetlem3  20293  mp2pm2mplem4  20433  chfacfisf  20478  chfacfisfcpmat  20479  cpmadugsumlemF  20500  elcls  20687  leordtval  20827  cnpnei  20878  cnco  20880  cnss1  20890  cmpsub  21013  hauscmplem  21019  dissnlocfin  21142  ptbasid  21188  tx2cn  21223  upxp  21236  txindis  21247  xkoptsub  21267  xkopt  21268  trfbas2  21457  filcon  21497  trfil2  21501  filssufilg  21525  ufileu  21533  fixufil  21536  ufilen  21544  rnelfmlem  21566  flimclsi  21592  hauspwpwf1  21601  fclsopn  21628  fclsfnflim  21641  fclscmpi  21643  alexsubALTlem3  21663  alexsubALTlem4  21664  ptcmplem5  21670  tgpmulg  21707  subgtgp  21719  tgpt0  21732  tsmsxplem2  21767  metss  22123  metustfbas  22172  dscopn  22188  xrsmopn  22423  cncfss  22510  icoopnst  22546  iccpnfcnv  22551  icccvx  22557  evth  22566  phtpycc  22598  pcohtpylem  22627  lmmbrf  22868  fgcfil  22877  caucfil  22889  cfilres  22902  bcth3  22936  ovolfioo  23043  ovolficc  23044  voliunlem3  23127  volcn  23180  mbflimsup  23239  mbfi1fseqlem5  23292  itg2seq  23315  dvnff  23492  dvnadd  23498  cpnord  23504  c1liplem1  23563  plypf1  23772  plyaddlem1  23773  plymullem1  23774  coeeulem  23784  coeidlem  23797  dgrle  23803  dgrnznn  23807  plycjlem  23836  elqaalem3  23880  ulmcaulem  23952  ulmcau  23953  psergf  23970  psercn2  23981  efopn  24204  abscxpbnd  24294  leibpi  24469  isppw2  24641  muinv  24719  bposlem3  24811  gausslemma2dlem4  24894  pntrmax  25053  pntpbnd1  25075  qabvexp  25115  eqeelen  25584  colinearalglem4  25589  axcgrid  25596  axsegconlem1  25597  axsegconlem3  25599  ax5seglem1  25608  ax5seglem2  25609  ax5seglem9  25617  axcontlem2  25645  usgraidx2vlem2  25921  cusgrares  26001  cusgrafilem2  26008  wlkiswwlk1  26218  wwlkextproplem3  26271  el2wlkonot  26396  el2spthonot0  26398  usgravd00  26446  rusgraprop4  26471  eupath2lem3  26506  frgrancvvdeqlemB  26565  frgrawopreglem5  26575  frghash2spot  26590  numclwwlkun  26606  numclwwlkovf2ex  26613  grpoidinvlem3  26744  grpoidinv  26746  grpoideu  26747  nmoub3i  27012  nmlno0lem  27032  nmlnoubi  27035  ipasslem3  27072  ipblnfi  27095  hvaddsub4  27319  his35  27329  shsel3  27558  chj4  27778  spansncol  27811  chscllem2  27881  5oalem2  27898  3oalem2  27906  hoaddcl  28001  adjsym  28076  cnvadj  28135  hhcno  28147  hhcnf  28148  nmopub2tALT  28152  unoplin  28163  counop  28164  nmfnleub2  28169  hmoplin  28185  brafnmul  28194  nmlnop0iALT  28238  nmopun  28257  nmophmi  28274  riesz3i  28305  riesz1  28308  cnlnadjlem2  28311  cnlnadjlem6  28315  adjmul  28335  adjadd  28336  bra11  28351  cnvbraval  28353  kbass5  28363  kbass6  28364  leop2  28367  leopadd  28375  leopmuli  28376  leoptri  28379  leopnmid  28381  nmopleid  28382  pj3si  28450  hstel2  28462  cvcon3  28527  dmdmd  28543  dmdbr5  28551  mdsl0  28553  mdslmd1lem1  28568  mdslmd1lem2  28569  mdslmd3i  28575  superpos  28597  chirredlem2  28634  chirredlem3  28635  mdsymlem3  28648  mdsymlem5  28650  mdsymlem6  28651  sumdmdlem  28661  cdjreui  28675  cdj1i  28676  cdj3i  28684  foresf1o  28727  abfmpel  28835  fcomptf  28840  fcnvgreu  28855  xrge0infss  28915  cmpcref  29245  xrge0iifcnv  29307  esumcst  29452  hasheuni  29474  esum2dlem  29481  esum2d  29482  sigaclcu2  29510  insiga  29527  unelldsys  29548  measres  29612  measdivcst  29615  volfiniune  29620  ddemeas  29626  sgn3da  29930  sconpi1  30475  cvmsss2  30510  mrsubco  30672  dfon2lem6  30937  dftrpred3g  30977  poseq  30994  soseq  30995  nodenselem3  31082  nobndlem6  31096  hfext  31460  elicc3  31481  fnessref  31522  fin2solem  32565  fin2so  32566  lindsenlbs  32574  matunitlindflem1  32575  matunitlindflem2  32576  poimirlem2  32581  poimirlem14  32593  poimirlem25  32604  poimirlem26  32605  poimirlem29  32608  poimirlem30  32609  broucube  32613  heicant  32614  mblfinlem2  32617  mblfinlem3  32618  mblfinlem4  32619  ex-ovoliunnfl  32622  mbfresfi  32626  cnambfre  32628  itg2addnclem  32631  itg2addnclem2  32632  itg2addnc  32634  bddiblnc  32650  ftc1anclem3  32657  ftc1anclem4  32658  ftc1anclem5  32659  ftc1anclem6  32660  ftc1anclem7  32661  ftc1anclem8  32662  ftc1anc  32663  eqfnun  32686  indexdom  32699  filbcmb  32705  fdc  32711  incsequz  32714  metf1o  32721  caures  32726  bndss  32755  ismtycnv  32771  heiborlem1  32780  rrncmslem  32801  isdrngo2  32927  rngoisocnv  32950  unichnidl  33000  ax12eq  33244  ax12el  33245  lshpset2N  33424  pmapglb2N  34075  pmapglb2xN  34076  pclfinN  34204  polval2N  34210  cdleme31fv2  34699  cdleme32fvcl  34746  cdleme48gfv  34843  tendoicl  35102  tendoipl  35103  diaglbN  35362  dochkr1  35785  dochkr1OLDN  35786  nacsfix  36293  eq0rabdioph  36358  diophren  36395  rencldnfilem  36402  pell1234qrdich  36443  jm2.24  36548  jm2.26lem3  36586  wepwsolem  36630  pwssplit4  36677  isnumbasgrplem3  36694  cvgdvgrat  37534  ofsubid  37545  bcc0  37561  binomcxplemnn0  37570  uzwo4  38246  fiiuncl  38259  iunincfi  38300  nsstr  38301  rexanuz3  38303  disjrnmpt2  38370  fompt  38374  disjinfi  38375  mapsnd  38383  choicefi  38387  fsneq  38393  difmap  38394  iunmapsn  38404  axccdom  38411  axccd  38424  ssfiunibd  38464  supxrgelem  38494  suplesup  38496  xrlexaddrp  38509  xralrple2  38511  infxrunb2  38525  xralrple3  38531  xrralrecnnle  38543  xrralrecnnge  38554  iooiinicc  38616  ressioosup  38629  iooiinioc  38630  ressiooinf  38631  fsumsplitsn  38637  fsumsupp0  38645  divcnvg  38694  limcrecl  38696  sumnnodd  38697  islpcn  38706  lptre2pt  38707  limcresiooub  38709  limcresioolb  38710  limclner  38718  fnlimfvre  38741  allbutfifvre  38742  cncfuni  38772  icccncfext  38773  cncficcgt0  38774  cncfiooicclem1  38779  cncfiooiccre  38781  dvasinbx  38810  dvdsn1add  38829  dvnmul  38833  dvmptfprodlem  38834  dvnprodlem1  38836  dvnprodlem3  38838  iblspltprt  38865  itgioocnicc  38869  itgspltprt  38871  ismbl3  38879  stirlinglem5  38971  dirker2re  38985  dirkerper  38989  dirkertrigeq  38994  dirkercncflem2  38997  fourierdlem12  39012  fourierdlem15  39015  fourierdlem16  39016  fourierdlem20  39020  fourierdlem21  39021  fourierdlem22  39022  fourierdlem39  39039  fourierdlem40  39040  fourierdlem41  39041  fourierdlem42  39042  fourierdlem46  39045  fourierdlem49  39048  fourierdlem50  39049  fourierdlem57  39056  fourierdlem58  39057  fourierdlem59  39058  fourierdlem64  39063  fourierdlem65  39064  fourierdlem66  39065  fourierdlem68  39067  fourierdlem70  39069  fourierdlem71  39070  fourierdlem73  39072  fourierdlem78  39077  fourierdlem79  39078  fourierdlem80  39079  fourierdlem81  39080  fourierdlem82  39081  fourierdlem83  39082  fourierdlem87  39086  fourierdlem93  39092  fourierdlem95  39094  fourierdlem101  39100  fourierdlem103  39102  fourierdlem104  39103  fourierdlem111  39110  fourierdlem112  39111  sqwvfoura  39121  fourierswlem  39123  elaa2lem  39126  etransclem13  39140  etransclem23  39150  etransclem24  39151  etransclem32  39159  etransclem38  39165  etransclem46  39173  qndenserrnbllem  39190  rrxsnicc  39196  ioorrnopnlem  39200  prsal  39214  intsal  39224  salexct  39228  dfsalgen2  39235  issalnnd  39239  sge0rnre  39257  sge0val  39259  sge0z  39268  sge0revalmpt  39271  sge0tsms  39273  sge0pr  39287  sge0resplit  39299  sge0split  39302  sge0splitmpt  39304  sge0iunmptlemfi  39306  sge0iunmptlemre  39308  sge0fodjrnlem  39309  sge0iunmpt  39311  sge0rpcpnf  39314  sge0ltfirpmpt2  39319  sge0isum  39320  sge0xaddlem1  39326  sge0xaddlem2  39327  sge0pnffsumgt  39335  sge0gtfsumgt  39336  sge0seq  39339  sge0reuz  39340  nnfoctbdjlem  39348  nnfoctbdj  39349  meadjun  39355  meadjiunlem  39358  voliunsge0lem  39365  omeiunltfirp  39409  carageniuncllem2  39412  caratheodorylem1  39416  caratheodorylem2  39417  caratheodory  39418  isomenndlem  39420  isomennd  39421  hoicvr  39438  volicorescl  39443  ovnsubaddlem2  39461  hoidmvlelem2  39486  hoidmvlelem3  39487  hoidmvle  39490  ovnhoilem2  39492  hspdifhsp  39506  hoiqssbllem2  39513  hoiqssbllem3  39514  hspmbllem2  39517  ovnsubadd2lem  39535  ovolval4lem1  39539  vonvolmbl  39551  vonioo  39573  vonicc  39576  pimrecltpos  39596  issmfle  39632  smflimlem1  39657  smflimlem2  39658  smflimlem6  39662  smfresal  39673  smfrec  39674  smfmullem4  39679  smonoord  39944  fmtnoprmfac1  40015  fmtnofac2lem  40018  bgoldbst  40200  lswn0  40242  2f1fvneq  40322  f1cofveqaeq  40323  egrsubgr  40501  cusgrfilem2  40672  vtxdgfisf  40691  usgr2pthlem  40969  uspgrn2crct  41011  crctcsh1wlkn0  41024  wwlksnextproplem3  41117  eupth2lem3lem4  41399  frgr3vlem1  41443  frgr3vlem2  41444  3vfriswmgrlem  41447  frgrhash2wsp  41497  av-extwwlkfablem2  41510  av-numclwwlkovf2ex  41517  av-numclwwlk3lem  41538  resmgmhm  41588  resmgmhm2b  41590  mgmhmco  41591  mgmhmima  41592  snlindsntorlem  42053  aacllem  42356
  Copyright terms: Public domain W3C validator