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

Theorem 3adant1 1153
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.) (Proof shortened by Wolf Lammen, 21-Jun-2022.)
Hypothesis
Ref Expression
3adant.1 ((𝜑𝜓) → 𝜒)
Assertion
Ref Expression
3adant1 ((𝜃𝜑𝜓) → 𝜒)

Proof of Theorem 3adant1
StepHypRef Expression
1 3adant.1 . . 3 ((𝜑𝜓) → 𝜒)
21adantll 696 . 2 (((𝜃𝜑) ∧ 𝜓) → 𝜒)
323impa 1129 1 ((𝜃𝜑𝜓) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1100
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 198  df-an 385  df-3an 1102
This theorem is referenced by:  3ad2ant2  1157  3ad2ant3  1158  3simpc  1175  eupickb  2700  sbciegft  3662  reuhyp  5091  funopg  6133  funprg  6152  funtpg  6153  funcnvtp  6161  fvun1  6488  fnreseql  6547  ftpg  6645  f13dfv  6752  mpt2eq3ia  6948  ordunel  7255  fex2  7349  poxp  7521  suppval1  7533  wfr3g  7646  smores3  7684  oaord  7862  oacan  7863  oaword  7864  omord  7883  omcan  7884  omwordri  7887  odi  7894  omass  7895  oeord  7903  oecan  7904  oewordri  7907  oeordsuc  7909  nnaord  7934  nnaordr  7935  nndi  7938  nnmass  7939  nnaword  7942  nnmord  7947  nnmwordri  7951  erov  8078  ecopovtrn  8084  ixpf  8165  mapxpen  8363  fimax2g  8443  unbnn  8453  funisfsupp  8517  inelfi  8561  elfiun  8573  sup0  8609  suppr  8614  infpr  8646  r111  8883  dif1card  9114  xpcdaen  9288  mapcdaen  9289  ackbij1lem16  9340  cff1  9363  cfflb  9364  cfsmolem  9375  fin23lem34  9451  hsmexlem2  9532  axcc3  9543  domtriomlem  9547  axdc3lem4  9558  axdc4lem  9560  axcclem  9562  konigthlem  9673  gchdomtri  9734  tskpr  9875  tskop  9876  tskuni  9888  tskun  9891  gruop  9910  gruun  9911  grudomon  9922  adderpqlem  10059  mulerpqlem  10060  addassnq  10063  mulassnq  10064  distrnq  10066  ltsonq  10074  ltanq  10076  ltmnq  10077  genpass  10114  distrlem1pr  10130  distrlem4pr  10131  ltsopr  10137  adddir  10314  axlttrn  10393  ltletr  10412  letr  10414  mul32  10486  mul31  10487  add32  10537  subsub23  10569  addsubass  10574  subcan2  10589  subsub2  10592  nppcan2  10595  sub32  10598  nnncan  10599  nnncan2  10601  pnpcan2  10604  subdi  10746  subdir  10747  receu  10955  mulcan1g  10963  mulcan2g  10964  divmul3  10973  divrec  10984  divrec2  10985  divsubdir  11004  divdiv1  11019  redivcl  11027  div2neg  11031  ltmul2  11157  lemul1  11158  lemul2  11159  lemul2a  11161  lediv1  11171  gt0div  11172  ge0div  11173  mulsuble0b  11178  ltdivmul  11181  ledivmul  11182  ltdivmul2  11183  ledivmul2  11185  lemuldiv  11186  ltdiv23  11197  lediv23  11198  ledivp1i  11232  ltdivp1i  11233  uzind2  11734  nn0ind  11736  fnn0ind  11740  uz3m2nn  11947  xrltletr  12204  xrletr  12205  xrre2  12217  xrltmin  12229  xrlemin  12231  xleadd2a  12300  xleadd1  12301  xltadd2  12303  xmulasslem3  12332  xmulass  12333  xltmul2  12339  ixxdisj  12406  iooneg  12511  iccneg  12512  icoshft  12513  icoshftf1o  12514  icodisj  12516  snunioo  12519  fzen  12579  ssfzunsnext  12607  fzrev3  12627  2ffzeq  12682  fzoaddel2  12746  elfzodifsumelfzo  12756  ssfzoulel  12784  ssfzo12bi  12785  fzoshftral  12807  adddivflid  12841  flltdivnn0lt  12856  ltdifltdiv  12857  fldiv4p1lem1div2  12858  modcyc  12927  modcyc2  12928  modaddabs  12930  modsubmodmod  12951  modaddmodup  12955  modaddmulmod  12959  moddi  12960  modsubdir  12961  expdiv  13132  digit2  13218  nfile  13366  hashdifpr  13418  hashreshashfun  13441  fi1uzind  13494  ccatass  13583  lswccatn0lsw  13586  swrdval  13638  swrdnd  13654  swrd0  13656  swrdfv2  13668  2swrd1eqwrdeq  13676  swrdswrdlem  13681  swrdccatin12lem2a  13707  swrdccatin12lem2b  13708  repswccat  13754  cshwidxmod  13771  cshwidxmodr  13772  cshf1  13778  repswcshw  13780  2cshw  13781  2cshwcom  13784  2cshwcshw  13793  cshwcsh2id  13796  ccatco  13803  2swrd2eqwrdeq  13919  wwlktovf  13922  brcnvtrclfv  13965  shftval2  14036  mulre  14082  absdiv  14256  absdiflt  14278  absdifle  14279  abs3dif  14292  cau3  14316  ello12r  14469  elo12r  14480  modfsummods  14745  geoisum1c  14831  rpnnen2lem4  15164  rpnnen2lem7  15167  dvdsmulc  15230  dvdsmulcr  15232  dvdsmultr1  15240  dvdsmultr2  15242  dvdssub2  15244  oexpneg  15287  divalgb  15345  ndvdsadd  15351  sadass  15410  modgcd  15470  dvdsgcd  15478  dvdsgcdb  15479  gcdass  15481  mulgcd  15482  absmulgcd  15483  rpmulgcd  15492  nn0seqcvgd  15500  algcvga  15509  lcmdvdsb  15543  lcmass  15544  lcmfunsnlem1  15567  lcmfunsnlem2lem1  15568  lcmfunsnlem2lem2  15569  coprmdvds  15583  coprmdvds2  15584  rpmul  15589  cncongr1  15597  cncongr2  15598  prmgt1  15625  qnumdenbi  15667  modprm0  15725  coprimeprodsq  15728  pythagtriplem4  15739  pythagtriplem8  15743  pythagtriplem9  15744  pythagtriplem12  15746  pythagtriplem14  15748  pythagtriplem16  15750  pcpremul  15763  pcgcd  15797  vdwapval  15892  vdwapun  15893  prmgaplem3  15972  prmgaplem4  15973  prmgaplem7  15976  prmgapprmolem  15980  setsstructOLD  16108  mreiincl  16459  mreincl  16462  mremre  16467  mrcss  16479  catcisolem  16958  pleval2  17168  pospo  17176  latlem  17252  latjcom  17262  latmcom  17278  lubss  17324  lubun  17326  clatglbss  17330  ipole  17361  ipolt  17362  pslem  17409  dirtr  17439  gsumws2  17582  frmdmnd  17599  isgrpi  17648  grpsubrcan  17699  grpinvsub  17700  grpsubeq0  17704  grpsubadd0sub  17705  grpnpcan  17710  qussub  17854  ghmsub  17868  symggrp  18019  symgextsymg  18043  gsmsymgreqlem2  18050  symgfixfolem1  18057  pmtrprfv3  18073  symggen  18089  lsmass  18282  efgsrel  18346  cntzcmn  18444  dvrcl  18886  unitdvcl  18887  dvrcan1  18891  subrgmre  19006  abvsubtri  19037  abvtrivd  19042  lmodvsubval2  19120  rmodislmodlem  19132  rmodislmod  19133  lss0cl  19149  lssintcl  19169  lssincl  19170  reslmhm2  19258  lspvadd  19301  lspsntrim  19303  islbs3  19362  rrgeq0  19497  evlsval2  19726  cncrng  19973  xrsmcmn  19975  cndrng  19981  cnsrng  19986  xrs1mnd  19990  absabv  20009  psgnco  20134  zrhpsgninv  20136  zrhpsgnevpm  20142  zrhpsgnodpm  20143  zrhpsgnelbas  20146  zrhcopsgnelbas  20147  uvcresum  20340  lindfmm  20374  lindsmm  20375  mamudm  20402  mamufacex  20403  matsubgcell  20448  matsc  20465  scmatscmide  20522  scmatrhmcl  20543  1marepvsma1  20598  m1detdiag  20612  mdetralt  20623  m2detleiblem7  20642  gsummatr01lem3  20673  gsummatr01  20675  smadiadetlem0  20677  decpmate  20782  decpmatcl  20783  pm2mpcl  20813  pm2mpghmlem2  20828  chfacfscmul0  20874  chfacfscmulgsum  20876  chfacfpmmul0  20878  chfacfpmmulgsum  20880  unopn  20919  clsss  21070  cldmre  21094  toponmre  21109  opnssneib  21131  restabs  21181  restcls  21197  restntr  21198  hausnei2  21369  cmpsublem  21414  bwth  21425  hausmapdom  21515  ptpjcn  21626  upxp  21638  ptrescn  21654  xkopjcn  21671  fbssfi  21852  snfil  21879  ufprim  21924  rnelfm  21968  flimrest  21998  fclsrest  22039  tmdgsum  22110  blpnfctr  22452  mscl  22477  xmscl  22478  xmsge0  22479  xmseq0  22480  restmetu  22586  ngpds  22619  tngngp3  22671  unitnmn0  22683  xrsxmet  22823  metds0  22864  cncfmptc  22925  isclmp  23107  cnlmod  23150  ncvsi  23161  cphsqrtcl  23194  cfil3i  23277  cfilres  23304  cmmbl  23513  voliunlem2  23530  itg2ub  23712  itgrecl  23776  tdeglem3  24031  r1pid  24131  eflogeq  24560  cxpadd  24637  logbchbase  24721  relogbreexp  24725  relogbzexp  24726  relogbmulexp  24728  logbleb  24733  logblt  24734  lawcos  24758  pythag  24759  asinsinb  24836  acoscosb  24837  atantanb  24863  amgmlem  24928  lgsneg  25258  lgsne0  25272  lgsmodeq  25279  lgsmulsqcoprm  25280  gausslemma2dlem1a  25302  brbtwn2  25997  colinearalg  26002  eleesubd  26004  axcgrrflx  26006  axcgrtr  26007  axsegcon  26019  ax5seglem1  26020  ax5seglem2  26021  ax5seglem4  26024  axbtwnid  26031  axlowdimlem14  26047  axlowdim  26053  axcontlem5  26060  axcontlem7  26062  funvtxdmge2valOLD  26111  funiedgdmge2valOLD  26112  usgr1v0e  26432  nb3grprlem2  26497  cplgr3v  26557  cusgrsizeindslem  26573  sizusglecusglem2  26584  umgr2v2e  26647  cusgrrusgr  26703  iswlk  26732  edginwlk  26756  uspgr2wlkeq  26768  uspgr2wlkeq2  26769  uspgr2wlkeqi  26770  wlkon2n0  26788  pthdadjvtx  26852  upgr2pthnlp  26854  spthonepeq  26874  pthdlem2lem  26889  crctcshwlkn0lem3  26931  crctcshwlkn0lem5  26933  wlkiswwlks2lem4  26997  wlkiswwlks2lem6  26999  wlklnwwlkln2lem  27007  wwlksnred  27027  wwlksnextbi  27029  wwlksnextwrd  27032  2pthdlem1  27068  2wlkdlem10  27073  umgr2adedgwlkonALT  27085  elwwlks2s3  27089  elwwlks2ons3im  27092  elwwlks2ons3OLD  27094  s3wwlks2on  27095  2wspdisj  27102  2wspiundisj  27103  clwwlkgt0  27127  clwlkclwwlklem2a4  27138  clwlkclwwlklem2a  27139  clwlkclwwlk  27143  clwlkclwwlk2  27144  clwlkclwwlkfo  27150  clwwisshclwwslemlem  27154  erclwwlktr  27163  clwwlkf  27194  wwlksubclwwlk  27207  erclwwlkntr  27220  clwlksfclwwlkOLD  27234  clwwlknon  27253  clwwlknonwwlknonbOLD  27273  frcond1  27439  frgr3v  27448  3vfriswmgr  27451  frgrwopreglem4a  27483  frrusgrord0lem  27512  clwwnonrepclwwnon  27520  extwwlkfab  27529  numclwwlk1lem2f1  27534  numclwwlk1lem2fo  27535  clwlknon2num  27546  numclwwlk2lem1  27554  numclwlk2lem2f  27555  numclwlk2lem2f1o  27557  numclwwlk2  27559  numclwwlk2lem1OLD  27561  numclwlk2lem2fOLD  27562  numclwlk2lem2f1oOLD  27564  numclwwlk2OLD  27566  frgrreggt1  27579  friendshipgt3  27584  imsmetlem  27871  nmoxr  27947  nmoolb  27952  blometi  27984  phpar2  28004  phpar  28005  ipasslem5  28016  hvadd32  28217  hvaddsub12  28221  hvaddsubass  28224  hvsubass  28227  hvsub32  28228  hvsubdistr1  28232  hvsubdistr2  28233  hvmulcan  28255  hvmulcan2  28256  hvsubcan  28257  his5  28269  his2sub  28275  hhssabloilem  28444  hhssnv  28447  shlej2  28546  pjoi0  28902  hodcl  28932  hoadd32  28968  hosubdi  28993  hosubsub2  28997  hoaddsubass  29000  hosubsub4  29003  nmoplb  29092  unop  29100  hmop  29107  nmfnlb  29109  lnopmul  29152  kbass1  29301  kbass2  29302  leopmul2i  29320  leoptr  29322  cvntr  29477  mdslmd4i  29518  mdexchi  29520  atcv1  29565  sumdmdii  29600  fcoinvbr  29742  fpwrelmapffs  29834  xreceu  29953  isinftm  30058  unitdivcld  30270  esummulc1  30466  hasheuni  30470  unelsiga  30520  inelpisys  30540  carsgsigalem  30700  signswmnd  30957  bnj545  31286  bnj594  31303  bnj1311  31413  cvmsf1o  31575  cvmscld  31576  lediv2aALT  31891  subdivcomb2  31932  gcd32  31957  fununiq  31987  trpredpo  32053  poseq  32072  frr3g  32098  sltres  32134  sltletr  32200  sletr  32202  nocvxmin  32213  dfrdg4  32377  brcolinear  32485  colinearex  32486  nn0prpwlem  32636  clsun  32642  fnemeet1  32680  fnemeet2  32681  fnejoin1  32682  fnejoin2  32683  eltail  32688  rdgeqoa  33532  curf  33698  poimirlem28  33748  cnambfre  33768  ftc1anclem4  33798  cocanfo  33822  f1ocan1fv  33831  metf1o  33860  ismtybnd  33915  ghomco  33999  isdrngo2  34066  inidl  34138  igenmin  34172  brxrn  34447  cmtvalN  34989  cvrval  35047  pmapmeet  35551  paddval  35576  paddssat  35592  elpcliN  35671  pclssN  35672  pclunN  35676  paddunN  35705  poldmj1N  35706  tendoplcl2  36557  tendoplcl  36560  dihmeet  37122  mapco2g  37777  mzpcompact2lem  37814  eqrabdioph  37841  lerabdioph  37869  eluzrabdioph  37870  ltrabdioph  37872  nerabdioph  37873  dvdsrabdioph  37874  reglogcl  37954  rmxyadd  37985  rmyabs  38024  congadd  38032  congabseq  38040  rmydioph  38080  mendring  38261  mendlmod  38262  iocinico  38295  relexp0a  38506  relexpaddss  38508  brcoffn  38826  dvconstbi  39031  uzwo4  39712  ssin0  39714  ssinc  39755  ssdec  39756  unima  39833  fvmpt2bd  39837  disjf1o  39865  ssnnf1octb  39869  sub31  39983  fperiodmullem  39996  ssfiunibd  40002  infxr  40061  fmul01  40290  islptre  40329  lptre2pt  40350  limcleqr  40354  limclner  40361  limsuppnflem  40420  limsupvaluz2  40448  supcnvlimsup  40450  xlimmnfvlem2  40537  xlimmnfv  40538  xlimpnfvlem2  40541  xlimpnfv  40542  climxlim2lem  40549  coskpi2  40555  cosknegpi  40558  dvnmptdivc  40631  dvdsn1add  40632  dvnmptconst  40634  dvmptfprod  40638  dvnprodlem1  40639  dvnprodlem2  40640  ovolsplit  40682  stoweidlem60  40754  stowei  40758  dirkeritg  40796  fourierdlem70  40870  fourierdlem71  40871  fourierdlem103  40903  fourierdlem104  40904  fouriersw  40925  rrxtopnfi  40983  saluncl  41014  salexct  41029  sge0ltfirp  41094  sge0iunmpt  41112  meadjiunlem  41159  meaiuninc3v  41178  carageniuncllem1  41215  caratheodorylem1  41220  ovncvrrp  41258  ovnsubaddlem1  41264  hspmbllem2  41321  ovolval5lem3  41348  smfpimbor1lem1  41485  smfsuplem1  41497  smflimsuplem4  41509  sigarls  41526  cnambpcma  41883  elfzelfzlble  41904  fzoopth  41910  m1mod0mod1  41912  fsumsplitsndif  41916  iccpartiltu  41931  pfxsuff1eqwrdeq  41980  ccatpfx  41982  pfx2  41985  pfxccatin12lem1  41996  fmtno4prmfac  42057  2pwp1prmfmtno  42077  lighneallem4b  42099  mogoldbblem  42202  gbegt5  42222  sbgoldbm  42245  nnsum3primesle9  42255  nnsum4primesodd  42257  nnsum4primesoddALTV  42258  evengpoap3  42260  nnsum4primesevenALTV  42262  isupwlk  42283  lidldomnnring  42496  2zrngacmnd  42508  rhmsubclem2  42653  rhmsubcALTVlem2  42671  xpprsng  42676  zlmodzxzscm  42701  gsumlsscl  42730  lincvalsng  42771  lincvalpr  42773  lincdifsn  42779  linc1  42780  lincellss  42781  difmodm1lt  42883  fdivmpt  42900  digexp  42967  amgmwlem  43117
  Copyright terms: Public domain W3C validator