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

Theorem 3adant1 1124
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 693 . 2 (((𝜃𝜑) ∧ 𝜓) → 𝜒)
323impa 1100 1 ((𝜃𝜑𝜓) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1071
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 383  df-3an 1073
This theorem is referenced by:  3ad2ant2  1128  3ad2ant3  1129  3simpc  1146  eupickb  2687  sbciegft  3618  reuhyp  5024  funopg  6065  funprg  6083  funtpg  6084  funcnvtp  6092  fvun1  6411  fnreseql  6470  ftpg  6566  f13dfv  6673  mpt2eq3ia  6867  ordunel  7174  fex2  7268  poxp  7440  suppval1  7452  wfr3g  7565  smores3  7603  oaord  7781  oacan  7782  oaword  7783  omord  7802  omcan  7803  omwordri  7806  odi  7813  omass  7814  oeord  7822  oecan  7823  oewordri  7826  oeordsuc  7828  nnaord  7853  nnaordr  7854  nndi  7857  nnmass  7858  nnaword  7861  nnmord  7866  nnmwordri  7870  erov  7997  ecopovtrn  8003  ixpf  8084  mapxpen  8282  fimax2g  8362  unbnn  8372  funisfsupp  8436  inelfi  8480  elfiun  8492  sup0  8528  suppr  8533  infpr  8565  r111  8802  dif1card  9033  xpcdaen  9207  mapcdaen  9208  ackbij1lem16  9259  cff1  9282  cfflb  9283  cfsmolem  9294  fin23lem34  9370  hsmexlem2  9451  axcc3  9462  domtriomlem  9466  axdc3lem4  9477  axdc4lem  9479  axcclem  9481  konigthlem  9592  gchdomtri  9653  tskpr  9794  tskop  9795  tskuni  9807  tskun  9810  gruop  9829  gruun  9830  grudomon  9841  adderpqlem  9978  mulerpqlem  9979  addassnq  9982  mulassnq  9983  distrnq  9985  ltsonq  9993  ltanq  9995  ltmnq  9996  genpass  10033  distrlem1pr  10049  distrlem4pr  10050  ltsopr  10056  adddir  10233  axlttrn  10312  ltletr  10331  letr  10333  mul32  10405  mul31  10406  add32  10456  subsub23  10488  addsubass  10493  subcan2  10508  subsub2  10511  nppcan2  10514  sub32  10517  nnncan  10518  nnncan2  10520  pnpcan2  10523  subdi  10665  subdir  10666  receu  10874  mulcan1g  10882  mulcan2g  10883  divmul3  10892  divrec  10903  divrec2  10904  divsubdir  10923  divdiv1  10938  redivcl  10946  div2neg  10950  ltmul2  11076  lemul1  11077  lemul2  11078  lemul2a  11080  lediv1  11090  gt0div  11091  ge0div  11092  mulsuble0b  11097  ltdivmul  11100  ledivmul  11101  ltdivmul2  11102  ledivmul2  11104  lemuldiv  11105  ltdiv23  11116  lediv23  11117  ledivp1i  11151  ltdivp1i  11152  uzind2  11672  nn0ind  11674  fnn0ind  11678  uz3m2nn  11933  xrltletr  12193  xrletr  12194  xrre2  12206  xrltmin  12218  xrlemin  12220  xleadd2a  12289  xleadd1  12290  xltadd2  12292  xmulasslem3  12321  xmulass  12322  xltmul2  12328  ixxdisj  12395  iooneg  12499  iccneg  12500  icoshft  12501  icoshftf1o  12502  icodisj  12504  snunioo  12505  fzen  12565  ssfzunsnext  12593  fzrev3  12613  2ffzeq  12668  fzoaddel2  12732  elfzodifsumelfzo  12742  ssfzoulel  12770  ssfzo12bi  12771  fzoshftral  12793  adddivflid  12827  flltdivnn0lt  12842  ltdifltdiv  12843  fldiv4p1lem1div2  12844  modcyc  12913  modcyc2  12914  modaddabs  12916  modsubmodmod  12937  modaddmodup  12941  modaddmulmod  12945  moddi  12946  modsubdir  12947  expdiv  13118  digit2  13204  nfile  13352  hashdifpr  13405  hashreshashfun  13428  fi1uzind  13481  ccatass  13570  lswccatn0lsw  13573  swrdval  13625  swrdnd  13641  swrd0  13643  swrdfv2  13655  2swrd1eqwrdeq  13663  swrdswrdlem  13668  swrdccatin12lem2a  13694  swrdccatin12lem2b  13695  repswccat  13741  cshwidxmod  13758  cshwidxmodr  13759  cshf1  13765  repswcshw  13767  2cshw  13768  2cshwcom  13771  2cshwcshw  13780  cshwcsh2id  13783  ccatco  13790  2swrd2eqwrdeq  13906  wwlktovf  13909  brcnvtrclfv  13952  shftval2  14023  mulre  14069  absdiv  14243  absdiflt  14265  absdifle  14266  abs3dif  14279  cau3  14303  ello12r  14456  elo12r  14467  modfsummods  14732  geoisum1c  14818  rpnnen2lem4  15152  rpnnen2lem7  15155  dvdsmulc  15218  dvdsmulcr  15220  dvdsmultr1  15228  dvdsmultr2  15230  dvdssub2  15232  oexpneg  15277  divalgb  15335  ndvdsadd  15342  sadass  15401  modgcd  15461  dvdsgcd  15469  dvdsgcdb  15470  gcdass  15472  mulgcd  15473  absmulgcd  15474  rpmulgcd  15483  nn0seqcvgd  15491  algcvga  15500  lcmdvdsb  15534  lcmass  15535  lcmfunsnlem1  15558  lcmfunsnlem2lem1  15559  lcmfunsnlem2lem2  15560  coprmdvds  15574  coprmdvds2  15575  rpmul  15580  cncongr1  15588  cncongr2  15589  prmgt1  15616  qnumdenbi  15659  modprm0  15717  coprimeprodsq  15720  pythagtriplem4  15731  pythagtriplem8  15735  pythagtriplem9  15736  pythagtriplem12  15738  pythagtriplem14  15740  pythagtriplem16  15742  pcpremul  15755  pcgcd  15789  vdwapval  15884  vdwapun  15885  prmgaplem3  15964  prmgaplem4  15965  prmgaplem7  15968  prmgapprmolem  15972  setsstructOLD  16106  mreiincl  16464  mreincl  16467  mremre  16472  mrcss  16484  catcisolem  16963  pleval2  17173  pospo  17181  latlem  17257  latjcom  17267  latmcom  17283  lubss  17329  lubun  17331  clatglbss  17335  ipole  17366  ipolt  17367  pslem  17414  dirtr  17444  gsumws2  17587  frmdmnd  17604  isgrpi  17653  grpsubrcan  17704  grpinvsub  17705  grpsubeq0  17709  grpsubadd0sub  17710  grpnpcan  17715  qussub  17862  ghmsub  17876  symggrp  18027  symgextsymg  18051  gsmsymgreqlem2  18058  symgfixfolem1  18065  pmtrprfv3  18081  symggen  18097  lsmass  18290  efgsrel  18354  cntzcmn  18452  dvrcl  18894  unitdvcl  18895  dvrcan1  18899  subrgmre  19014  abvsubtri  19045  abvtrivd  19050  lmodvsubval2  19128  rmodislmodlem  19140  rmodislmod  19141  lss0cl  19157  lssintcl  19177  lssincl  19178  reslmhm2  19266  lspvadd  19309  lspsntrim  19311  islbs3  19370  rrgeq0  19505  evlsval2  19735  cncrng  19982  xrsmcmn  19984  cndrng  19990  cnsrng  19995  xrs1mnd  19999  absabv  20018  psgnco  20144  zrhpsgninv  20146  zrhpsgnevpm  20152  zrhpsgnodpm  20153  zrhpsgnelbas  20156  zrhcopsgnelbas  20157  uvcresum  20349  lindfmm  20383  lindsmm  20384  mamudm  20411  mamufacex  20412  matsubgcell  20457  matsc  20474  scmatscmide  20531  scmatrhmcl  20552  1marepvsma1  20607  m1detdiag  20621  mdetralt  20632  m2detleiblem7  20651  gsummatr01lem3  20682  gsummatr01  20684  smadiadetlem0  20686  decpmate  20791  decpmatcl  20792  pm2mpcl  20822  pm2mpghmlem2  20837  chfacfscmul0  20883  chfacfscmulgsum  20885  chfacfpmmul0  20887  chfacfpmmulgsum  20889  unopn  20928  clsss  21079  cldmre  21103  toponmre  21118  opnssneib  21140  restabs  21190  restcls  21206  restntr  21207  hausnei2  21378  cmpsublem  21423  bwth  21434  hausmapdom  21524  ptpjcn  21635  upxp  21647  ptrescn  21663  xkopjcn  21680  fbssfi  21861  snfil  21888  ufprim  21933  rnelfm  21977  flimrest  22007  fclsrest  22048  tmdgsum  22119  blpnfctr  22461  mscl  22486  xmscl  22487  xmsge0  22488  xmseq0  22489  restmetu  22595  ngpds  22628  tngngp3  22680  unitnmn0  22692  xrsxmet  22832  metds0  22873  cncfmptc  22934  isclmp  23116  cnlmod  23159  ncvsi  23170  cphsqrtcl  23203  cfil3i  23286  cfilres  23313  cmmbl  23522  voliunlem2  23539  itg2ub  23720  itgrecl  23784  tdeglem3  24039  r1pid  24139  eflogeq  24569  cxpadd  24646  logbchbase  24730  relogbreexp  24734  relogbzexp  24735  relogbmulexp  24737  logbleb  24742  logblt  24743  lawcos  24767  pythag  24768  asinsinb  24845  acoscosb  24846  atantanb  24872  amgmlem  24937  lgsneg  25267  lgsne0  25281  lgsmodeq  25288  lgsmulsqcoprm  25289  gausslemma2dlem1a  25311  brbtwn2  26006  colinearalg  26011  eleesubd  26013  axcgrrflx  26015  axcgrtr  26016  axsegcon  26028  ax5seglem1  26029  ax5seglem2  26030  ax5seglem4  26033  axbtwnid  26040  axlowdimlem14  26056  axlowdim  26062  axcontlem5  26069  axcontlem7  26071  funvtxdmge2valOLD  26120  funiedgdmge2valOLD  26121  usgr1v0e  26441  nb3grprlem2  26506  cplgr3v  26566  cusgrsizeindslem  26582  sizusglecusglem2  26593  umgr2v2e  26656  cusgrrusgr  26712  iswlk  26741  edginwlk  26765  uspgr2wlkeq  26777  uspgr2wlkeq2  26778  uspgr2wlkeqi  26779  wlkon2n0  26797  pthdadjvtx  26861  upgr2pthnlp  26863  spthonepeq  26883  pthdlem2lem  26898  crctcshwlkn0lem3  26940  crctcshwlkn0lem5  26942  wlkiswwlks2lem4  27006  wlkiswwlks2lem6  27008  wlklnwwlkln2lem  27016  wwlksnred  27036  wwlksnextbi  27038  wwlksnextwrd  27041  2pthdlem1  27077  2wlkdlem10  27082  umgr2adedgwlkonALT  27094  elwwlks2s3  27098  elwwlks2ons3im  27101  elwwlks2ons3OLD  27103  s3wwlks2on  27104  2wspdisj  27111  2wspiundisj  27112  clwwlkgt0  27136  clwlkclwwlklem2a4  27147  clwlkclwwlklem2a  27148  clwlkclwwlk  27152  clwlkclwwlk2  27153  clwlkclwwlkfo  27159  clwwisshclwwslemlem  27163  erclwwlktr  27172  clwwlkf  27203  wwlksubclwwlk  27216  erclwwlkntr  27229  clwlksfclwwlkOLD  27243  clwwlknon  27262  clwwlknonwwlknonbOLD  27282  frcond1  27448  frgr3v  27457  3vfriswmgr  27460  frgrwopreglem4a  27492  frrusgrord0lem  27521  clwwnonrepclwwnon  27529  extwwlkfab  27538  numclwwlk1lem2f1  27543  numclwwlk1lem2fo  27544  clwlknon2num  27559  numclwwlk2lem1  27567  numclwlk2lem2f  27568  numclwlk2lem2f1o  27570  numclwwlk2  27572  numclwwlk2lem1OLD  27574  numclwlk2lem2fOLD  27575  numclwlk2lem2f1oOLD  27577  numclwwlk2OLD  27579  frgrreggt1  27592  friendshipgt3  27597  imsmetlem  27885  nmoxr  27961  nmoolb  27966  blometi  27998  phpar2  28018  phpar  28019  ipasslem5  28030  hvadd32  28231  hvaddsub12  28235  hvaddsubass  28238  hvsubass  28241  hvsub32  28242  hvsubdistr1  28246  hvsubdistr2  28247  hvmulcan  28269  hvmulcan2  28270  hvsubcan  28271  his5  28283  his2sub  28289  hhssabloilem  28458  hhssnv  28461  shlej2  28560  pjoi0  28916  hodcl  28946  hoadd32  28982  hosubdi  29007  hosubsub2  29011  hoaddsubass  29014  hosubsub4  29017  nmoplb  29106  unop  29114  hmop  29121  nmfnlb  29123  lnopmul  29166  kbass1  29315  kbass2  29316  leopmul2i  29334  leoptr  29336  cvntr  29491  mdslmd4i  29532  mdexchi  29534  atcv1  29579  sumdmdii  29614  fcoinvbr  29757  fpwrelmapffs  29849  xreceu  29970  isinftm  30075  unitdivcld  30287  esummulc1  30483  hasheuni  30487  unelsiga  30537  inelpisys  30557  carsgsigalem  30717  signswmnd  30974  bnj545  31303  bnj594  31320  bnj1311  31430  cvmsf1o  31592  cvmscld  31593  lediv2aALT  31909  subdivcomb2  31950  gcd32  31975  fununiq  32005  trpredpo  32071  poseq  32090  frr3g  32116  sltres  32152  sltletr  32218  sletr  32220  nocvxmin  32231  dfrdg4  32395  brcolinear  32503  colinearex  32504  nn0prpwlem  32654  clsun  32660  fnemeet1  32698  fnemeet2  32699  fnejoin1  32700  fnejoin2  32701  eltail  32706  rdgeqoa  33555  curf  33720  poimirlem28  33770  cnambfre  33790  ftc1anclem4  33820  cocanfo  33844  f1ocan1fv  33853  metf1o  33883  ismtybnd  33938  ghomco  34022  isdrngo2  34089  inidl  34161  igenmin  34195  brxrn  34478  cmtvalN  35020  cvrval  35078  pmapmeet  35581  paddval  35606  paddssat  35622  elpcliN  35701  pclssN  35702  pclunN  35706  paddunN  35735  poldmj1N  35736  tendoplcl2  36587  tendoplcl  36590  dihmeet  37153  mapco2g  37803  mzpcompact2lem  37840  eqrabdioph  37867  lerabdioph  37895  eluzrabdioph  37896  ltrabdioph  37898  nerabdioph  37899  dvdsrabdioph  37900  reglogcl  37980  rmxyadd  38012  rmyabs  38051  congadd  38059  congabseq  38067  rmydioph  38107  mendring  38288  mendlmod  38289  iocinico  38323  relexp0a  38534  relexpaddss  38536  brcoffn  38854  dvconstbi  39059  uzwo4  39742  ssin0  39744  ssinc  39785  ssdec  39786  unima  39866  fvmpt2bd  39870  disjf1o  39898  ssnnf1octb  39902  sub31  40021  fperiodmullem  40034  ssfiunibd  40040  infxr  40099  fmul01  40330  islptre  40369  lptre2pt  40390  limcleqr  40394  limclner  40401  limsuppnflem  40460  limsupvaluz2  40488  supcnvlimsup  40490  xlimmnfvlem2  40577  xlimmnfv  40578  xlimpnfvlem2  40581  xlimpnfv  40582  climxlim2lem  40589  coskpi2  40595  cosknegpi  40598  dvnmptdivc  40671  dvdsn1add  40672  dvnmptconst  40674  dvmptfprod  40678  dvnprodlem1  40679  dvnprodlem2  40680  ovolsplit  40722  stoweidlem60  40794  stowei  40798  dirkeritg  40836  fourierdlem70  40910  fourierdlem71  40911  fourierdlem103  40943  fourierdlem104  40944  fouriersw  40965  rrxtopnfi  41023  saluncl  41054  salexct  41069  sge0ltfirp  41134  sge0iunmpt  41152  meadjiunlem  41199  meaiuninc3v  41218  carageniuncllem1  41255  caratheodorylem1  41260  ovncvrrp  41298  ovnsubaddlem1  41304  hspmbllem2  41361  ovolval5lem3  41388  smfpimbor1lem1  41525  smfsuplem1  41537  smflimsuplem4  41549  sigarls  41566  cnambpcma  41837  elfzelfzlble  41859  fzoopth  41865  m1mod0mod1  41867  fsumsplitsndif  41871  iccpartiltu  41886  pfxsuff1eqwrdeq  41935  ccatpfx  41937  pfx2  41940  pfxccatin12lem1  41951  fmtno4prmfac  42012  2pwp1prmfmtno  42032  lighneallem4b  42054  mogoldbblem  42157  gbegt5  42177  sbgoldbm  42200  nnsum3primesle9  42210  nnsum4primesodd  42212  nnsum4primesoddALTV  42213  evengpoap3  42215  nnsum4primesevenALTV  42217  isupwlk  42245  lidldomnnring  42458  2zrngacmnd  42470  rhmsubclem2  42615  rhmsubcALTVlem2  42633  xpprsng  42638  zlmodzxzscm  42663  gsumlsscl  42692  lincvalsng  42733  lincvalpr  42735  lincdifsn  42741  linc1  42742  lincellss  42743  difmodm1lt  42845  fdivmpt  42862  digexp  42929  amgmwlem  43079
  Copyright terms: Public domain W3C validator