Theorem 3adant1 1131

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 1110	1 ⊢ ((𝜃 ∧ 𝜑 ∧ 𝜓) → 𝜒)

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

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 1089

This theorem is referenced by:  3ad2ant2  1135  3ad2ant3  1136  3simpc  1151  eupickb  2635  spc3egv  3603  sbciegftOLD  3826  reuhyp  5420  predtrss  6343  onunel  6489  funopg  6600  funprg  6620  funtpg  6621  funcnvtp  6629  unima  6984  fvun1  7000  fnreseql  7068  xpprsng  7160  ftpg  7176  f1ounsn  7292  f13dfv  7294  f1ocoima  7323  f1ofvswap  7326  mpoeq3ia  7511  ordunel  7847  fex2  7958  funexw  7976  poxp  8153  poxp2  8168  poxp3  8175  poseq  8183  suppval1  8191  wfr3g  8347  smores3  8393  oaord  8585  oacan  8586  oaword  8587  omord  8606  omcan  8607  omwordri  8610  odi  8617  omass  8618  oeord  8626  oecan  8627  oewordri  8630  oeordsuc  8632  nnaord  8657  nnaordr  8658  nndi  8661  nnmass  8662  nnaword  8665  nnmord  8670  nnmwordri  8674  naddelim  8724  naddel1  8725  naddel2  8726  naddss1  8727  naddss2  8728  naddasslem2  8733  nadd32  8735  erov  8854  ecopovtrn  8860  ixpf  8960  f1oen4g  9005  f1dom4g  9006  mapxpen  9183  dif1enlemOLD  9197  ssfi  9213  sbthfilem  9238  sbthfi  9239  onomeneq  9265  fimax2g  9322  unbnn  9332  funisfsupp  9407  inelfi  9458  elfiun  9470  sup0  9506  suppr  9511  infpr  9543  ttrclss  9760  frr3g  9796  r111  9815  dif1card  10050  ackbij1lem16  10274  cff1  10298  cfflb  10299  cfsmolem  10310  fin23lem34  10386  hsmexlem2  10467  axcc3  10478  domtriomlem  10482  axdc3lem4  10493  axdc4lem  10495  axcclem  10497  konigthlem  10608  gchdomtri  10669  tskpr  10810  tskop  10811  tskuni  10823  tskun  10826  gruop  10845  gruun  10846  grudomon  10857  adderpqlem  10994  mulerpqlem  10995  addassnq  10998  mulassnq  10999  distrnq  11001  ltsonq  11009  ltanq  11011  ltmnq  11012  genpass  11049  distrlem1pr  11065  distrlem4pr  11066  ltsopr  11072  adddir  11252  axlttrn  11333  ltletr  11353  letr  11355  mul32  11427  mul31  11428  add32  11480  subsub23  11513  addsubass  11518  subcan2  11534  subsub2  11537  nppcan2  11540  sub32  11543  nnncan  11544  nnncan2  11546  pnpcan2  11549  subdi  11696  subdir  11697  receu  11908  mulcan1g  11916  mulcan2g  11917  divmul3  11927  divrec  11938  divrec2  11939  div11  11950  divsubdir  11961  subdivcomb2  11963  divdiv1  11978  redivcl  11986  div2neg  11990  ltmul2  12118  lemul1  12119  lemul2  12120  lemul2a  12122  lediv1  12133  gt0div  12134  ge0div  12135  mulsuble0b  12140  ltdivmul  12143  ledivmul  12144  ltdivmul2  12145  ledivmul2  12147  lemuldiv  12148  ltdiv23  12159  lediv23  12160  ledivp1i  12193  ltdivp1i  12194  uzind2  12711  nn0ind  12713  fnn0ind  12717  uz3m2nn  12933  xrltletr  13199  xrletr  13200  xrre2  13212  xrltmin  13224  xrlemin  13226  xleadd2a  13296  xleadd1  13297  xltadd2  13299  xmulasslem3  13328  xmulass  13329  xltmul2  13335  ixxdisj  13402  iooneg  13511  iccneg  13512  icoshft  13513  icoshftf1o  13514  icodisj  13516  snunioo  13518  fzen  13581  ssfzunsnext  13609  fzrev3  13630  2ffzeq  13689  fzoaddel2  13759  elfzodifsumelfzo  13770  ssfzoulel  13799  ssfzo12bi  13800  fzoopth  13801  fzoshftral  13823  adddivflid  13858  flltdivnn0lt  13873  ltdifltdiv  13874  fldiv4p1lem1div2  13875  modcyc  13946  modcyc2  13947  modaddabs  13949  muladdmod  13953  modsubmodmod  13971  modaddmodup  13975  modaddmulmod  13979  moddi  13980  modsubdir  13981  expdiv  14154  digit2  14275  nfile  14398  hashdifpr  14454  hashgt23el  14463  hashreshashfun  14478  hashf1dmcdm  14483  hash3tpexb  14533  fi1uzind  14546  ccatval1  14615  ccatass  14626  swrdval  14681  swrdnd  14692  swrd0  14696  swrdfv2  14699  pfxsuff1eqwrdeq  14737  swrdswrdlem  14742  pfxccatin12lem2a  14765  pfxccatin12lem1  14766  repswccat  14824  cshwidxmod  14841  cshwidxmodr  14842  cshf1  14848  repswcshw  14850  2cshw  14851  2cshwcom  14854  2cshwcshw  14864  cshwcsh2id  14867  ccatco  14874  2swrd2eqwrdeq  14992  wwlktovf  14995  brcnvtrclfv  15042  shftval2  15114  mulre  15160  absdiv  15334  absdiflt  15356  absdifle  15357  abs3dif  15370  cau3  15394  ello12r  15553  elo12r  15564  modfsummods  15829  geoisum1c  15916  rpnnen2lem4  16253  rpnnen2lem7  16256  addmulmodb  16303  dvdsmulc  16321  dvdsmulcr  16323  dvdsmultr1  16333  dvdsmultr2  16335  dvdssub2  16338  oexpneg  16382  divalgb  16441  ndvdsadd  16447  sadass  16508  modgcd  16569  dvdsgcd  16581  dvdsgcdb  16582  gcdass  16584  mulgcd  16585  absmulgcd  16586  rpmulgcd  16594  expgcd  16600  zexpgcd  16602  nn0seqcvgd  16607  algcvga  16616  lcmdvdsb  16650  lcmass  16651  lcmfunsnlem1  16674  lcmfunsnlem2lem1  16675  lcmfunsnlem2lem2  16676  coprmdvds  16690  coprmdvds2  16691  rpmul  16696  cncongr1  16704  cncongr2  16705  qnumdenbi  16781  modprm0  16843  coprimeprodsq  16846  pythagtriplem4  16857  pythagtriplem8  16861  pythagtriplem9  16862  pythagtriplem12  16864  pythagtriplem14  16866  pythagtriplem16  16868  pcpremul  16881  pcgcd  16916  vdwapval  17011  vdwapun  17012  prmgaplem3  17091  prmgaplem4  17092  prmgaplem7  17095  prmgapprmolem  17099  mreiincl  17639  mreincl  17642  mremre  17647  mrcss  17659  catcisolem  18155  pleval2  18382  pospo  18390  latlem  18482  latjcom  18492  latmcom  18508  lubss  18558  lubun  18560  clatglbss  18564  ipole  18579  ipolt  18580  pslem  18617  dirtr  18647  gsumsgrpccat  18853  gsumws2  18855  frmdmnd  18872  symggrplem  18897  isgrpi  18977  grpsubrcan  19039  grpinvsub  19040  grpsubeq0  19044  grpsubadd0sub  19045  grpnpcan  19050  qussub  19209  ghmsub  19242  symgpssefmnd  19413  symggrp  19418  symgextsymg  19442  gsmsymgreqlem2  19449  symgfixfolem1  19456  pmtrprfv3  19472  symggen  19488  lsmass  19687  efgsrel  19752  cntzcmn  19858  dvrcl  20404  unitdvcl  20405  dvrcan1  20409  subrngmre  20562  subrgmre  20597  rhmsubclem2  20686  rrgeq0  20700  abvsubtri  20828  abvtrivd  20833  lmodvsubval2  20915  rmodislmodlem  20927  rmodislmod  20928  lss0cl  20945  lssintcl  20962  lssincl  20963  reslmhm2  21052  lspvadd  21095  lspsntrim  21097  islbs3  21157  rnglidlmmgm  21255  cncrng  21401  cncrngOLD  21402  xrsmcmn  21404  cndrng  21411  cndrngOLD  21412  cnsrng  21418  xrs1mnd  21422  absabv  21442  psgnco  21601  zrhpsgninv  21603  zrhpsgnevpm  21609  zrhpsgnodpm  21610  zrhpsgnelbas  21612  zrhcopsgnelbas  21613  uvcresum  21813  lindfmm  21847  lindsmm  21848  evlsval2  22111  mamudm  22399  mamufacex  22400  matsubgcell  22440  matsc  22456  scmatscmide  22513  scmatrhmcl  22534  1marepvsma1  22589  m1detdiag  22603  mdetralt  22614  m2detleiblem7  22633  gsummatr01lem3  22663  gsummatr01  22665  smadiadetlem0  22667  decpmate  22772  decpmatcl  22773  pm2mpcl  22803  pm2mpghmlem2  22818  chfacfscmul0  22864  chfacfscmulgsum  22866  chfacfpmmul0  22868  chfacfpmmulgsum  22870  unopn  22909  clsss  23062  cldmre  23086  toponmre  23101  opnssneib  23123  restabs  23173  restcls  23189  restntr  23190  hausnei2  23361  cmpsublem  23407  bwth  23418  hausmapdom  23508  ptpjcn  23619  upxp  23631  ptrescn  23647  xkopjcn  23664  fbssfi  23845  snfil  23872  ufprim  23917  rnelfm  23961  flimrest  23991  fclsrest  24032  tmdgsum  24103  blpnfctr  24446  mscl  24471  xmscl  24472  xmsge0  24473  xmseq0  24474  restmetu  24583  ngpds  24617  tngngp3  24677  unitnmn0  24689  xrsxmet  24831  metds0  24872  mpomulcn  24891  cncfmptc  24938  isclmp  25130  cnlmod  25173  ncvsi  25185  cphsqrtcl  25218  cfil3i  25303  cfilres  25330  cmssmscld  25384  cmmbl  25569  voliunlem2  25586  itg2ub  25768  itgrecl  25833  r1pid  26200  eflogeq  26644  cxpadd  26721  cxpcom  26781  logbchbase  26814  relogbreexp  26818  relogbzexp  26819  relogbmulexp  26821  logbleb  26826  logblt  26827  lawcos  26859  pythag  26860  asinsinb  26940  acoscosb  26941  atantanb  26967  amgmlem  27033  lgsneg  27365  lgsne0  27379  lgsmodeq  27386  lgsmulsqcoprm  27387  gausslemma2dlem1a  27409  2sqreulem2  27496  sltres  27707  noetainflem1  27782  sltletr  27801  sletr  27803  nocvxmin  27823  madebdaylemold  27936  lrrecpo  27974  sltadd2im  28019  sleadd1im  28020  sleadd2im  28021  sleadd1  28022  sleadd2  28023  sltadd1  28025  addscan2  28026  addscan1  28027  subadds  28100  sltsub1  28106  divscl  28247  nohalf  28407  0reno  28429  brbtwn2  28920  colinearalg  28925  eleesubd  28927  axcgrrflx  28929  axcgrtr  28930  axsegcon  28942  ax5seglem1  28943  ax5seglem2  28944  ax5seglem4  28947  axbtwnid  28954  axlowdimlem14  28970  axlowdim  28976  axcontlem5  28983  axcontlem7  28985  nb3grprlem2  29398  cplgr3v  29452  cusgrsizeindslem  29469  sizusglecusglem2  29480  umgr2v2e  29543  cusgrrusgr  29599  iswlk  29628  edginwlk  29653  uspgr2wlkeq  29664  uspgr2wlkeq2  29665  uspgr2wlkeqi  29666  wlkonprop  29676  wlkon2n0  29684  pthdadjvtx  29748  upgr2pthnlp  29752  spthonepeq  29772  pthdlem2lem  29787  crctcshwlkn0lem3  29832  crctcshwlkn0lem5  29834  wlkiswwlks2lem4  29892  wlkiswwlks2lem6  29894  wlklnwwlkln2lem  29902  wwlksnred  29912  wwlksnextbi  29914  wwlksnextwrd  29917  2pthdlem1  29950  2wlkdlem10  29955  umgr2adedgwlkonALT  29967  elwwlks2s3  29971  elwwlks2ons3im  29974  s3wwlks2on  29976  2wspdisj  29982  2wspiundisj  29983  clwwlkgt0  30005  clwlkclwwlklem2a4  30016  clwlkclwwlklem2a  30017  clwlkclwwlk  30021  clwlkclwwlk2  30022  clwlkclwwlkfo  30028  clwwisshclwwslemlem  30032  erclwwlktr  30041  clwwlkf  30066  wwlksubclwwlk  30077  erclwwlkntr  30090  clwwlknon  30109  frcond1  30285  frgr3v  30294  3vfriswmgr  30297  frgrwopreglem4a  30329  frrusgrord0lem  30358  clwwnonrepclwwnon  30364  extwwlkfab  30371  numclwwlk1lem2f1  30376  numclwwlk1lem2fo  30377  clwlknon2num  30387  numclwwlk2lem1  30395  numclwlk2lem2f  30396  numclwlk2lem2f1o  30398  numclwwlk2  30400  frgrreggt1  30412  friendshipgt3  30417  imsmetlem  30709  nmoxr  30785  nmoolb  30790  blometi  30822  phpar2  30842  phpar  30843  ipasslem5  30854  hvadd32  31053  hvaddsub12  31057  hvaddsubass  31060  hvsubass  31063  hvsub32  31064  hvsubdistr1  31068  hvsubdistr2  31069  hvmulcan  31091  hvmulcan2  31092  hvsubcan  31093  his5  31105  his2sub  31111  hhssabloilem  31280  hhssnv  31283  shlej2  31380  pjoi0  31736  hodcl  31766  hoadd32  31802  hosubdi  31827  hosubsub2  31831  hoaddsubass  31834  hosubsub4  31837  nmoplb  31926  unop  31934  hmop  31941  nmfnlb  31943  lnopmul  31986  kbass1  32135  kbass2  32136  leopmul2i  32154  leoptr  32156  cvntr  32311  mdslmd4i  32352  mdexchi  32354  atcv1  32399  sumdmdii  32434  fcoinvbr  32618  fpwrelmapffs  32745  xreceu  32904  isinftm  33188  unitdivcld  33900  esummulc1  34082  hasheuni  34086  unelsiga  34135  inelpisys  34155  carsgsigalem  34317  signswmnd  34572  bnj545  34909  bnj594  34926  bnj1311  35038  fineqvac  35111  usgrgt2cycl  35135  subgrwlk  35137  acycgr1v  35154  cvmsf1o  35277  cvmscld  35278  satefvfmla1  35430  elnanelprv  35434  lediv2aALT  35682  gcd32  35749  fununiq  35769  dfrdg4  35952  brcolinear  36060  colinearex  36061  nn0prpwlem  36323  clsun  36329  fnemeet1  36367  fnemeet2  36368  fnejoin1  36369  fnejoin2  36370  eltail  36375  rdgeqoa  37371  nlpineqsn  37409  curf  37605  lindsadd  37620  poimirlem28  37655  cnambfre  37675  ftc1anclem4  37703  cocanfo  37726  f1ocan1fv  37733  metf1o  37762  ismtybnd  37814  ghomco  37898  isdrngo2  37965  inidl  38037  igenmin  38071  brxrn  38375  brredunds  38627  cmtvalN  39212  cvrval  39270  pmapmeet  39775  paddval  39800  paddssat  39816  elpcliN  39895  pclssN  39896  pclunN  39900  paddunN  39929  poldmj1N  39930  tendoplcl2  40780  tendoplcl  40783  dihmeet  41345  lcmineqlem1  42030  factwoffsmonot  42243  reltsub1  42416  reltsubadd2  42417  resubsub4  42419  reppncan  42423  resubdi  42426  readdcan2  42442  subresre  42460  mapco2g  42725  mzpcompact2lem  42762  eqrabdioph  42788  lerabdioph  42816  eluzrabdioph  42817  ltrabdioph  42819  nerabdioph  42820  dvdsrabdioph  42821  reglogcl  42901  rmxyadd  42933  rmyabs  42970  congadd  42978  congabseq  42986  rmydioph  43026  mendring  43200  mendlmod  43201  iocinico  43224  omge1  43310  relexp0a  43729  relexpaddss  43731  brcoffn  44043  ismnushort  44320  dvconstbi  44353  uzwo4  45058  ssin0  45060  ssinc  45092  ssdec  45093  fvmpt2bd  45175  disjf1o  45196  ssnnf1octb  45199  sub31  45302  fperiodmullem  45315  ssfiunibd  45321  infxr  45378  fmul01  45595  islptre  45634  lptre2pt  45655  limcleqr  45659  limclner  45666  limsuppnflem  45725  limsupvaluz2  45753  supcnvlimsup  45755  xlimmnfvlem2  45848  xlimmnfv  45849  xlimpnfvlem2  45852  xlimpnfv  45853  climxlim2lem  45860  coskpi2  45881  cosknegpi  45884  dvnmptdivc  45953  dvdsn1add  45954  dvnmptconst  45956  dvmptfprod  45960  dvnprodlem1  45961  dvnprodlem2  45962  ovolsplit  46003  stoweidlem60  46075  stowei  46079  dirkeritg  46117  fourierdlem70  46191  fourierdlem71  46192  fourierdlem103  46224  fourierdlem104  46225  fouriersw  46246  rrxtopnfi  46302  saluncl  46332  salexct  46349  sge0ltfirp  46415  sge0iunmpt  46433  meadjiunlem  46480  meaiuninc3v  46499  carageniuncllem1  46536  caratheodorylem1  46541  ovncvrrp  46579  ovnsubaddlem1  46585  hspmbllem2  46642  ovolval5lem3  46669  smfpimbor1lem1  46813  smfsuplem1  46826  smflimsuplem4  46838  sigarls  46872  cnambpcma  47306  elfzelfzlble  47333  submodaddmod  47343  difltmodne  47344  m1mod0mod1  47356  fsumsplitsndif  47360  fundcmpsurinjALT  47399  iccpartiltu  47409  prproropf1olem2  47491  fmtno4prmfac  47559  2pwp1prmfmtno  47577  lighneallem4b  47596  mogoldbblem  47707  gbegt5  47748  sbgoldbm  47771  nnsum3primesle9  47781  nnsum4primesodd  47783  nnsum4primesoddALTV  47784  evengpoap3  47786  nnsum4primesevenALTV  47788  clnbgredg  47826  opstrgric  47895  clnbgrgrimlem  47901  grtrif1o  47909  isubgr3stgrlem1  47933  isubgr3stgrlem4  47936  gpgusgralem  48011  gpg3nbgrvtx0  48032  isupwlk  48052  lidldomnnring  48152  2zrngacmnd  48164  rhmsubcALTVlem2  48198  fprmappr  48261  zlmodzxzscm  48273  gsumlsscl  48296  lincvalsng  48333  lincvalpr  48335  lincdifsn  48341  linc1  48342  lincellss  48343  difmodm1lt  48443  fdivmpt  48461  digexp  48528  2arymaptfo  48575  line  48653  rrxline  48655  itsclc0xyqsolr  48690  iscnrm3r  48845  amgmwlem  49321