Theorem 3adant1 1130

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

Step	Hyp	Ref	Expression
1		3adant.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	adantll 714	. 2 ⊢ (((𝜃 ∧ 𝜑) ∧ 𝜓) → 𝜒)
3	2	3impa 1109	1 ⊢ ((𝜃 ∧ 𝜑 ∧ 𝜓) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  3ad2ant2  1134  3ad2ant3  1135  3simpc  1150  eupickb  2629  spc3egv  3572  sbciegftOLD  3794  reuhyp  5378  predtrss  6298  onunel  6442  funopg  6553  funprg  6573  funtpg  6574  funcnvtp  6582  unima  6939  fvun1  6955  fnreseql  7023  xpprsng  7115  ftpg  7131  f1ounsn  7250  f13dfv  7252  f1ocoima  7281  f1ofvswap  7284  mpoeq3ia  7470  ordunel  7805  fex2  7915  funexw  7933  poxp  8110  poxp2  8125  poxp3  8132  poseq  8140  suppval1  8148  wfr3g  8301  smores3  8325  oaord  8514  oacan  8515  oaword  8516  omord  8535  omcan  8536  omwordri  8539  odi  8546  omass  8547  oeord  8555  oecan  8556  oewordri  8559  oeordsuc  8561  nnaord  8586  nnaordr  8587  nndi  8590  nnmass  8591  nnaword  8594  nnmord  8599  nnmwordri  8603  naddelim  8653  naddel1  8654  naddel2  8655  naddss1  8656  naddss2  8657  naddasslem2  8662  nadd32  8664  erov  8790  ecopovtrn  8796  ixpf  8896  f1oen4g  8939  f1dom4g  8940  mapxpen  9113  dif1enlemOLD  9127  ssfi  9143  sbthfilem  9168  sbthfi  9169  onomeneq  9184  fimax2g  9240  unbnn  9250  funisfsupp  9325  inelfi  9376  elfiun  9388  sup0  9425  suppr  9430  infpr  9463  ttrclss  9680  frr3g  9716  r111  9735  dif1card  9970  ackbij1lem16  10194  cff1  10218  cfflb  10219  cfsmolem  10230  fin23lem34  10306  hsmexlem2  10387  axcc3  10398  domtriomlem  10402  axdc3lem4  10413  axdc4lem  10415  axcclem  10417  konigthlem  10528  gchdomtri  10589  tskpr  10730  tskop  10731  tskuni  10743  tskun  10746  gruop  10765  gruun  10766  grudomon  10777  adderpqlem  10914  mulerpqlem  10915  addassnq  10918  mulassnq  10919  distrnq  10921  ltsonq  10929  ltanq  10931  ltmnq  10932  genpass  10969  distrlem1pr  10985  distrlem4pr  10986  ltsopr  10992  adddir  11172  axlttrn  11253  ltletr  11273  letr  11275  mul32  11347  mul31  11348  add32  11400  subsub23  11433  addsubass  11438  subcan2  11454  subsub2  11457  nppcan2  11460  sub32  11463  nnncan  11464  nnncan2  11466  pnpcan2  11469  subdi  11618  subdir  11619  receu  11830  mulcan1g  11838  mulcan2g  11839  divmul3  11849  divrec  11860  divrec2  11861  div11  11872  divsubdir  11883  subdivcomb2  11885  divdiv1  11900  redivcl  11908  div2neg  11912  ltmul2  12040  lemul1  12041  lemul2  12042  lemul2a  12044  lediv1  12055  gt0div  12056  ge0div  12057  mulsuble0b  12062  ltdivmul  12065  ledivmul  12066  ltdivmul2  12067  ledivmul2  12069  lemuldiv  12070  ltdiv23  12081  lediv23  12082  ledivp1i  12115  ltdivp1i  12116  uzind2  12634  nn0ind  12636  fnn0ind  12640  uz3m2nn  12860  xrltletr  13124  xrletr  13125  xrre2  13137  xrltmin  13149  xrlemin  13151  xleadd2a  13221  xleadd1  13222  xltadd2  13224  xmulasslem3  13253  xmulass  13254  xltmul2  13260  ixxdisj  13328  iooneg  13439  iccneg  13440  icoshft  13441  icoshftf1o  13442  icodisj  13444  snunioo  13446  fzen  13509  ssfzunsnext  13537  fzrev3  13558  2ffzeq  13617  fzoaddel2  13688  elfzodifsumelfzo  13699  ssfzoulel  13728  ssfzo12bi  13729  fzoopth  13730  fzoshftral  13752  adddivflid  13787  flltdivnn0lt  13802  ltdifltdiv  13803  fldiv4p1lem1div2  13804  modcyc  13875  modcyc2  13876  modaddabs  13880  muladdmod  13884  modsubmodmod  13902  modaddmodup  13906  modaddmulmod  13910  moddi  13911  modsubdir  13912  expdiv  14085  digit2  14208  nfile  14331  hashdifpr  14387  hashgt23el  14396  hashreshashfun  14411  hashf1dmcdm  14416  hash3tpexb  14466  fi1uzind  14479  ccatval1  14549  ccatass  14560  swrdval  14615  swrdnd  14626  swrd0  14630  swrdfv2  14633  pfxsuff1eqwrdeq  14671  swrdswrdlem  14676  pfxccatin12lem2a  14699  pfxccatin12lem1  14700  repswccat  14758  cshwidxmod  14775  cshwidxmodr  14776  cshf1  14782  repswcshw  14784  2cshw  14785  2cshwcom  14788  2cshwcshw  14798  cshwcsh2id  14801  ccatco  14808  2swrd2eqwrdeq  14926  wwlktovf  14929  brcnvtrclfv  14976  shftval2  15048  mulre  15094  absdiv  15268  absdiflt  15291  absdifle  15292  abs3dif  15305  cau3  15329  ello12r  15490  elo12r  15501  modfsummods  15766  geoisum1c  15853  rpnnen2lem4  16192  rpnnen2lem7  16195  addmulmodb  16242  dvdsmulc  16260  dvdsmulcr  16262  dvdsmultr1  16273  dvdsmultr2  16275  dvdssub2  16278  oexpneg  16322  divalgb  16381  ndvdsadd  16387  sadass  16448  modgcd  16509  dvdsgcd  16521  dvdsgcdb  16522  gcdass  16524  mulgcd  16525  absmulgcd  16526  rpmulgcd  16534  expgcd  16540  zexpgcd  16542  nn0seqcvgd  16547  algcvga  16556  lcmdvdsb  16590  lcmass  16591  lcmfunsnlem1  16614  lcmfunsnlem2lem1  16615  lcmfunsnlem2lem2  16616  coprmdvds  16630  coprmdvds2  16631  rpmul  16636  cncongr1  16644  cncongr2  16645  qnumdenbi  16721  modprm0  16783  coprimeprodsq  16786  pythagtriplem4  16797  pythagtriplem8  16801  pythagtriplem9  16802  pythagtriplem12  16804  pythagtriplem14  16806  pythagtriplem16  16808  pcpremul  16821  pcgcd  16856  vdwapval  16951  vdwapun  16952  prmgaplem3  17031  prmgaplem4  17032  prmgaplem7  17035  prmgapprmolem  17039  mreiincl  17564  mreincl  17567  mremre  17572  mrcss  17584  catcisolem  18079  pleval2  18303  pospo  18311  latlem  18403  latjcom  18413  latmcom  18429  lubss  18479  lubun  18481  clatglbss  18485  ipole  18500  ipolt  18501  pslem  18538  dirtr  18568  gsumsgrpccat  18774  gsumws2  18776  frmdmnd  18793  symggrplem  18818  isgrpi  18898  grpsubrcan  18960  grpinvsub  18961  grpsubeq0  18965  grpsubadd0sub  18966  grpnpcan  18971  qussub  19130  ghmsub  19163  symgpssefmnd  19333  symggrp  19337  symgextsymg  19361  gsmsymgreqlem2  19368  symgfixfolem1  19375  pmtrprfv3  19391  symggen  19407  lsmass  19606  efgsrel  19671  cntzcmn  19777  dvrcl  20320  unitdvcl  20321  dvrcan1  20325  subrngmre  20478  subrgmre  20513  rhmsubclem2  20602  rrgeq0  20616  abvsubtri  20743  abvtrivd  20748  lmodvsubval2  20830  rmodislmodlem  20842  rmodislmod  20843  lss0cl  20860  lssintcl  20877  lssincl  20878  reslmhm2  20967  lspvadd  21010  lspsntrim  21012  islbs3  21072  rnglidlmmgm  21162  cncrng  21307  cncrngOLD  21308  xrsmcmn  21310  cndrng  21317  cndrngOLD  21318  cnsrng  21324  xrs1mnd  21328  absabv  21348  psgnco  21499  zrhpsgninv  21501  zrhpsgnevpm  21507  zrhpsgnodpm  21508  zrhpsgnelbas  21510  zrhcopsgnelbas  21511  uvcresum  21709  lindfmm  21743  lindsmm  21744  evlsval2  22001  mamudm  22289  mamufacex  22290  matsubgcell  22328  matsc  22344  scmatscmide  22401  scmatrhmcl  22422  1marepvsma1  22477  m1detdiag  22491  mdetralt  22502  m2detleiblem7  22521  gsummatr01lem3  22551  gsummatr01  22553  smadiadetlem0  22555  decpmate  22660  decpmatcl  22661  pm2mpcl  22691  pm2mpghmlem2  22706  chfacfscmul0  22752  chfacfscmulgsum  22754  chfacfpmmul0  22756  chfacfpmmulgsum  22758  unopn  22797  clsss  22948  cldmre  22972  toponmre  22987  opnssneib  23009  restabs  23059  restcls  23075  restntr  23076  hausnei2  23247  cmpsublem  23293  bwth  23304  hausmapdom  23394  ptpjcn  23505  upxp  23517  ptrescn  23533  xkopjcn  23550  fbssfi  23731  snfil  23758  ufprim  23803  rnelfm  23847  flimrest  23877  fclsrest  23918  tmdgsum  23989  blpnfctr  24331  mscl  24356  xmscl  24357  xmsge0  24358  xmseq0  24359  restmetu  24465  ngpds  24499  tngngp3  24551  unitnmn0  24563  xrsxmet  24705  metds0  24746  mpomulcn  24765  cncfmptc  24812  isclmp  25004  cnlmod  25047  ncvsi  25058  cphsqrtcl  25091  cfil3i  25176  cfilres  25203  cmssmscld  25257  cmmbl  25442  voliunlem2  25459  itg2ub  25641  itgrecl  25706  r1pid  26073  eflogeq  26518  cxpadd  26595  cxpcom  26655  logbchbase  26688  relogbreexp  26692  relogbzexp  26693  relogbmulexp  26695  logbleb  26700  logblt  26701  lawcos  26733  pythag  26734  asinsinb  26814  acoscosb  26815  atantanb  26841  amgmlem  26907  lgsneg  27239  lgsne0  27253  lgsmodeq  27260  lgsmulsqcoprm  27261  gausslemma2dlem1a  27283  2sqreulem2  27370  sltres  27581  noetainflem1  27656  sltletr  27675  sletr  27677  nocvxmin  27697  madebdaylemold  27816  lrrecpo  27855  sltadd2im  27900  sleadd1im  27901  sleadd2im  27902  sleadd1  27903  sleadd2  27904  sltadd1  27906  addscan2  27907  addscan1  27908  subadds  27981  sltsub1  27987  divscl  28132  onscutlt  28172  expscllem  28323  0reno  28355  brbtwn2  28839  colinearalg  28844  eleesubd  28846  axcgrrflx  28848  axcgrtr  28849  axsegcon  28861  ax5seglem1  28862  ax5seglem2  28863  ax5seglem4  28866  axbtwnid  28873  axlowdimlem14  28889  axlowdim  28895  axcontlem5  28902  axcontlem7  28904  nb3grprlem2  29315  cplgr3v  29369  cusgrsizeindslem  29386  sizusglecusglem2  29397  umgr2v2e  29460  cusgrrusgr  29516  iswlk  29545  edginwlk  29570  uspgr2wlkeq  29581  uspgr2wlkeq2  29582  uspgr2wlkeqi  29583  wlkonprop  29593  wlkon2n0  29601  pthdadjvtx  29665  upgr2pthnlp  29669  spthonepeq  29689  pthdlem2lem  29704  crctcshwlkn0lem3  29749  crctcshwlkn0lem5  29751  wlkiswwlks2lem4  29809  wlkiswwlks2lem6  29811  wlklnwwlkln2lem  29819  wwlksnred  29829  wwlksnextbi  29831  wwlksnextwrd  29834  2pthdlem1  29867  2wlkdlem10  29872  umgr2adedgwlkonALT  29884  elwwlks2s3  29888  elwwlks2ons3im  29891  s3wwlks2on  29893  2wspdisj  29899  2wspiundisj  29900  clwwlkgt0  29922  clwlkclwwlklem2a4  29933  clwlkclwwlklem2a  29934  clwlkclwwlk  29938  clwlkclwwlk2  29939  clwlkclwwlkfo  29945  clwwisshclwwslemlem  29949  erclwwlktr  29958  clwwlkf  29983  wwlksubclwwlk  29994  erclwwlkntr  30007  clwwlknon  30026  frcond1  30202  frgr3v  30211  3vfriswmgr  30214  frgrwopreglem4a  30246  frrusgrord0lem  30275  clwwnonrepclwwnon  30281  extwwlkfab  30288  numclwwlk1lem2f1  30293  numclwwlk1lem2fo  30294  clwlknon2num  30304  numclwwlk2lem1  30312  numclwlk2lem2f  30313  numclwlk2lem2f1o  30315  numclwwlk2  30317  frgrreggt1  30329  friendshipgt3  30334  imsmetlem  30626  nmoxr  30702  nmoolb  30707  blometi  30739  phpar2  30759  phpar  30760  ipasslem5  30771  hvadd32  30970  hvaddsub12  30974  hvaddsubass  30977  hvsubass  30980  hvsub32  30981  hvsubdistr1  30985  hvsubdistr2  30986  hvmulcan  31008  hvmulcan2  31009  hvsubcan  31010  his5  31022  his2sub  31028  hhssabloilem  31197  hhssnv  31200  shlej2  31297  pjoi0  31653  hodcl  31683  hoadd32  31719  hosubdi  31744  hosubsub2  31748  hoaddsubass  31751  hosubsub4  31754  nmoplb  31843  unop  31851  hmop  31858  nmfnlb  31860  lnopmul  31903  kbass1  32052  kbass2  32053  leopmul2i  32071  leoptr  32073  cvntr  32228  mdslmd4i  32269  mdexchi  32271  atcv1  32316  sumdmdii  32351  fcoinvbr  32541  fpwrelmapffs  32664  xreceu  32849  isinftm  33142  unitdivcld  33898  esummulc1  34078  hasheuni  34082  unelsiga  34131  inelpisys  34151  carsgsigalem  34313  signswmnd  34555  bnj545  34892  bnj594  34909  bnj1311  35021  fineqvac  35094  usgrgt2cycl  35124  subgrwlk  35126  acycgr1v  35143  cvmsf1o  35266  cvmscld  35267  satefvfmla1  35419  elnanelprv  35423  lediv2aALT  35671  gcd32  35743  fununiq  35763  dfrdg4  35946  brcolinear  36054  colinearex  36055  nn0prpwlem  36317  clsun  36323  fnemeet1  36361  fnemeet2  36362  fnejoin1  36363  fnejoin2  36364  eltail  36369  rdgeqoa  37365  nlpineqsn  37403  curf  37599  lindsadd  37614  poimirlem28  37649  cnambfre  37669  ftc1anclem4  37697  cocanfo  37720  f1ocan1fv  37727  metf1o  37756  ismtybnd  37808  ghomco  37892  isdrngo2  37959  inidl  38031  igenmin  38065  brxrn  38363  brredunds  38624  cmtvalN  39211  cvrval  39269  pmapmeet  39774  paddval  39799  paddssat  39815  elpcliN  39894  pclssN  39895  pclunN  39899  paddunN  39928  poldmj1N  39929  tendoplcl2  40779  tendoplcl  40782  dihmeet  41344  lcmineqlem1  42024  reltsub1  42381  reltsubadd2  42382  resubsub4  42384  reppncan  42388  resubdi  42391  readdcan2  42408  subresre  42426  mapco2g  42709  mzpcompact2lem  42746  eqrabdioph  42772  lerabdioph  42800  eluzrabdioph  42801  ltrabdioph  42803  nerabdioph  42804  dvdsrabdioph  42805  reglogcl  42885  rmxyadd  42917  rmyabs  42954  congadd  42962  congabseq  42970  rmydioph  43010  mendring  43184  mendlmod  43185  iocinico  43208  omge1  43293  relexp0a  43712  relexpaddss  43714  brcoffn  44026  ismnushort  44297  dvconstbi  44330  uzwo4  45054  ssin0  45056  ssinc  45088  ssdec  45089  fvmpt2bd  45171  disjf1o  45192  ssnnf1octb  45195  sub31  45295  fperiodmullem  45308  ssfiunibd  45314  infxr  45370  fmul01  45585  islptre  45624  lptre2pt  45645  limcleqr  45649  limclner  45656  limsuppnflem  45715  limsupvaluz2  45743  supcnvlimsup  45745  xlimmnfvlem2  45838  xlimmnfv  45839  xlimpnfvlem2  45842  xlimpnfv  45843  climxlim2lem  45850  coskpi2  45871  cosknegpi  45874  dvnmptdivc  45943  dvdsn1add  45944  dvnmptconst  45946  dvmptfprod  45950  dvnprodlem1  45951  dvnprodlem2  45952  ovolsplit  45993  stoweidlem60  46065  stowei  46069  dirkeritg  46107  fourierdlem70  46181  fourierdlem71  46182  fourierdlem103  46214  fourierdlem104  46215  fouriersw  46236  rrxtopnfi  46292  saluncl  46322  salexct  46339  sge0ltfirp  46405  sge0iunmpt  46423  meadjiunlem  46470  meaiuninc3v  46489  carageniuncllem1  46526  caratheodorylem1  46531  ovncvrrp  46569  ovnsubaddlem1  46575  hspmbllem2  46632  ovolval5lem3  46659  smfpimbor1lem1  46803  smfsuplem1  46816  smflimsuplem4  46828  sigarls  46862  cnambpcma  47299  elfzelfzlble  47326  submodaddmod  47346  difltmodne  47347  m1mod0mod1  47359  modmkpkne  47366  mod2addne  47369  modm2nep1  47371  modm1nep2  47373  modm1nem2  47374  fsumsplitsndif  47378  fundcmpsurinjALT  47417  iccpartiltu  47427  prproropf1olem2  47509  fmtno4prmfac  47577  2pwp1prmfmtno  47595  lighneallem4b  47614  mogoldbblem  47725  gbegt5  47766  sbgoldbm  47789  nnsum3primesle9  47799  nnsum4primesodd  47801  nnsum4primesoddALTV  47802  evengpoap3  47804  nnsum4primesevenALTV  47806  clnbgredg  47844  opstrgric  47930  clnbgrgrimlem  47937  grtrif1o  47945  isubgr3stgrlem1  47969  isubgr3stgrlem4  47972  gpgusgralem  48051  gpg3nbgrvtx0  48071  isupwlk  48128  lidldomnnring  48228  2zrngacmnd  48240  rhmsubcALTVlem2  48274  fprmappr  48337  zlmodzxzscm  48349  gsumlsscl  48372  lincvalsng  48409  lincvalpr  48411  lincdifsn  48417  linc1  48418  lincellss  48419  fdivmpt  48533  digexp  48600  2arymaptfo  48647  line  48725  rrxline  48727  itsclc0xyqsolr  48762  iscnrm3r  48940  resipos  48967  amgmwlem  49795