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 713	. 2 ⊢ (((𝜃 ∧ 𝜑) ∧ 𝜓) → 𝜒)
3	2	3impa 1111	1 ⊢ ((𝜃 ∧ 𝜑 ∧ 𝜓) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  3ad2ant2  1135  3ad2ant3  1136  3simpc  1151  eupickb  2632  spc3egv  3594  sbciegft  3816  reuhyp  5419  predtrss  6324  onunel  6470  funopg  6583  funprg  6603  funtpg  6604  funcnvtp  6612  unima  6967  fvun1  6983  fnreseql  7050  xpprsng  7138  ftpg  7154  f13dfv  7272  f1ofvswap  7304  mpoeq3ia  7487  ordunel  7815  fex2  7924  funexw  7938  poxp  8114  poxp2  8129  poxp3  8136  poseq  8144  suppval1  8152  wfr3g  8307  smores3  8353  oaord  8547  oacan  8548  oaword  8549  omord  8568  omcan  8569  omwordri  8572  odi  8579  omass  8580  oeord  8588  oecan  8589  oewordri  8592  oeordsuc  8594  nnaord  8619  nnaordr  8620  nndi  8623  nnmass  8624  nnaword  8627  nnmord  8632  nnmwordri  8636  naddelim  8685  naddel1  8686  naddel2  8687  naddss1  8688  naddss2  8689  naddasslem2  8694  nadd32  8696  erov  8808  ecopovtrn  8814  ixpf  8914  f1oen4g  8960  f1dom4g  8961  mapxpen  9143  dif1enlemOLD  9157  ssfi  9173  sbthfilem  9201  sbthfi  9202  onomeneq  9228  fimax2g  9289  unbnn  9299  funisfsupp  9367  inelfi  9413  elfiun  9425  sup0  9461  suppr  9466  infpr  9498  ttrclss  9715  frr3g  9751  r111  9770  dif1card  10005  ackbij1lem16  10230  cff1  10253  cfflb  10254  cfsmolem  10265  fin23lem34  10341  hsmexlem2  10422  axcc3  10433  domtriomlem  10437  axdc3lem4  10448  axdc4lem  10450  axcclem  10452  konigthlem  10563  gchdomtri  10624  tskpr  10765  tskop  10766  tskuni  10778  tskun  10781  gruop  10800  gruun  10801  grudomon  10812  adderpqlem  10949  mulerpqlem  10950  addassnq  10953  mulassnq  10954  distrnq  10956  ltsonq  10964  ltanq  10966  ltmnq  10967  genpass  11004  distrlem1pr  11020  distrlem4pr  11021  ltsopr  11027  adddir  11205  axlttrn  11286  ltletr  11306  letr  11308  mul32  11380  mul31  11381  add32  11432  subsub23  11465  addsubass  11470  subcan2  11485  subsub2  11488  nppcan2  11491  sub32  11494  nnncan  11495  nnncan2  11497  pnpcan2  11500  subdi  11647  subdir  11648  receu  11859  mulcan1g  11867  mulcan2g  11868  divmul3  11877  divrec  11888  divrec2  11889  divsubdir  11908  subdivcomb2  11910  divdiv1  11925  redivcl  11933  div2neg  11937  ltmul2  12065  lemul1  12066  lemul2  12067  lemul2a  12069  lediv1  12079  gt0div  12080  ge0div  12081  mulsuble0b  12086  ltdivmul  12089  ledivmul  12090  ltdivmul2  12091  ledivmul2  12093  lemuldiv  12094  ltdiv23  12105  lediv23  12106  ledivp1i  12139  ltdivp1i  12140  uzind2  12655  nn0ind  12657  fnn0ind  12661  uz3m2nn  12875  xrltletr  13136  xrletr  13137  xrre2  13149  xrltmin  13161  xrlemin  13163  xleadd2a  13233  xleadd1  13234  xltadd2  13236  xmulasslem3  13265  xmulass  13266  xltmul2  13272  ixxdisj  13339  iooneg  13448  iccneg  13449  icoshft  13450  icoshftf1o  13451  icodisj  13453  snunioo  13455  fzen  13518  ssfzunsnext  13546  fzrev3  13567  2ffzeq  13622  fzoaddel2  13688  elfzodifsumelfzo  13698  ssfzoulel  13726  ssfzo12bi  13727  fzoshftral  13749  adddivflid  13783  flltdivnn0lt  13798  ltdifltdiv  13799  fldiv4p1lem1div2  13800  modcyc  13871  modcyc2  13872  modaddabs  13874  modsubmodmod  13895  modaddmodup  13899  modaddmulmod  13903  moddi  13904  modsubdir  13905  expdiv  14079  digit2  14199  nfile  14319  hashdifpr  14375  hashgt23el  14384  hashreshashfun  14399  fi1uzind  14458  ccatval1  14527  ccatass  14538  swrdval  14593  swrdnd  14604  swrd0  14608  swrdfv2  14611  pfxsuff1eqwrdeq  14649  swrdswrdlem  14654  pfxccatin12lem2a  14677  pfxccatin12lem1  14678  repswccat  14736  cshwidxmod  14753  cshwidxmodr  14754  cshf1  14760  repswcshw  14762  2cshw  14763  2cshwcom  14766  2cshwcshw  14776  cshwcsh2id  14779  ccatco  14786  2swrd2eqwrdeq  14904  wwlktovf  14907  brcnvtrclfv  14950  shftval2  15022  mulre  15068  absdiv  15242  absdiflt  15264  absdifle  15265  abs3dif  15278  cau3  15302  ello12r  15461  elo12r  15472  modfsummods  15739  geoisum1c  15826  rpnnen2lem4  16160  rpnnen2lem7  16163  dvdsmulc  16227  dvdsmulcr  16229  dvdsmultr1  16239  dvdsmultr2  16241  dvdssub2  16244  oexpneg  16288  divalgb  16347  ndvdsadd  16353  sadass  16412  modgcd  16474  dvdsgcd  16486  dvdsgcdb  16487  gcdass  16489  mulgcd  16490  absmulgcd  16491  rpmulgcd  16498  nn0seqcvgd  16507  algcvga  16516  lcmdvdsb  16550  lcmass  16551  lcmfunsnlem1  16574  lcmfunsnlem2lem1  16575  lcmfunsnlem2lem2  16576  coprmdvds  16590  coprmdvds2  16591  rpmul  16596  cncongr1  16604  cncongr2  16605  qnumdenbi  16680  modprm0  16738  coprimeprodsq  16741  pythagtriplem4  16752  pythagtriplem8  16756  pythagtriplem9  16757  pythagtriplem12  16759  pythagtriplem14  16761  pythagtriplem16  16763  pcpremul  16776  pcgcd  16811  vdwapval  16906  vdwapun  16907  prmgaplem3  16986  prmgaplem4  16987  prmgaplem7  16990  prmgapprmolem  16994  mreiincl  17540  mreincl  17543  mremre  17548  mrcss  17560  catcisolem  18060  pleval2  18290  pospo  18298  latlem  18390  latjcom  18400  latmcom  18416  lubss  18466  lubun  18468  clatglbss  18472  ipole  18487  ipolt  18488  pslem  18525  dirtr  18555  gsumsgrpccat  18721  gsumws2  18723  frmdmnd  18740  symggrplem  18765  isgrpi  18845  grpsubrcan  18904  grpinvsub  18905  grpsubeq0  18909  grpsubadd0sub  18910  grpnpcan  18915  qussub  19070  ghmsub  19100  symgpssefmnd  19263  symggrp  19268  symgextsymg  19292  gsmsymgreqlem2  19299  symgfixfolem1  19306  pmtrprfv3  19322  symggen  19338  lsmass  19537  efgsrel  19602  cntzcmn  19708  dvrcl  20218  unitdvcl  20219  dvrcan1  20223  subrgmre  20344  abvsubtri  20443  abvtrivd  20448  lmodvsubval2  20527  rmodislmodlem  20539  rmodislmod  20540  rmodislmodOLD  20541  lss0cl  20557  lssintcl  20575  lssincl  20576  reslmhm2  20664  lspvadd  20707  lspsntrim  20709  islbs3  20768  rrgeq0  20906  cncrng  20966  xrsmcmn  20968  cndrng  20974  cnsrng  20979  xrs1mnd  20983  absabv  21002  psgnco  21136  zrhpsgninv  21138  zrhpsgnevpm  21144  zrhpsgnodpm  21145  zrhpsgnelbas  21147  zrhcopsgnelbas  21148  uvcresum  21348  lindfmm  21382  lindsmm  21383  evlsval2  21650  mamudm  21890  mamufacex  21891  matsubgcell  21936  matsc  21952  scmatscmide  22009  scmatrhmcl  22030  1marepvsma1  22085  m1detdiag  22099  mdetralt  22110  m2detleiblem7  22129  gsummatr01lem3  22159  gsummatr01  22161  smadiadetlem0  22163  decpmate  22268  decpmatcl  22269  pm2mpcl  22299  pm2mpghmlem2  22314  chfacfscmul0  22360  chfacfscmulgsum  22362  chfacfpmmul0  22364  chfacfpmmulgsum  22366  unopn  22405  clsss  22558  cldmre  22582  toponmre  22597  opnssneib  22619  restabs  22669  restcls  22685  restntr  22686  hausnei2  22857  cmpsublem  22903  bwth  22914  hausmapdom  23004  ptpjcn  23115  upxp  23127  ptrescn  23143  xkopjcn  23160  fbssfi  23341  snfil  23368  ufprim  23413  rnelfm  23457  flimrest  23487  fclsrest  23528  tmdgsum  23599  blpnfctr  23942  mscl  23967  xmscl  23968  xmsge0  23969  xmseq0  23970  restmetu  24079  ngpds  24113  tngngp3  24173  unitnmn0  24185  xrsxmet  24325  metds0  24366  cncfmptc  24428  isclmp  24613  cnlmod  24656  ncvsi  24668  cphsqrtcl  24701  cfil3i  24786  cfilres  24813  cmssmscld  24867  cmmbl  25051  voliunlem2  25068  itg2ub  25251  itgrecl  25315  tdeglem3OLD  25576  r1pid  25677  eflogeq  26110  cxpadd  26187  cxpcom  26247  logbchbase  26276  relogbreexp  26280  relogbzexp  26281  relogbmulexp  26283  logbleb  26288  logblt  26289  lawcos  26321  pythag  26322  asinsinb  26402  acoscosb  26403  atantanb  26429  amgmlem  26494  lgsneg  26824  lgsne0  26838  lgsmodeq  26845  lgsmulsqcoprm  26846  gausslemma2dlem1a  26868  2sqreulem2  26955  sltres  27165  noetainflem1  27240  sltletr  27259  sletr  27261  nocvxmin  27280  madebdaylemold  27392  lrrecpo  27425  sltadd2im  27469  sleadd1im  27470  sleadd2im  27471  sleadd1  27472  sleadd2  27473  sltadd1  27475  addscan2  27476  addscan1  27477  subadds  27538  sltsub1  27543  divscl  27669  brbtwn2  28163  colinearalg  28168  eleesubd  28170  axcgrrflx  28172  axcgrtr  28173  axsegcon  28185  ax5seglem1  28186  ax5seglem2  28187  ax5seglem4  28190  axbtwnid  28197  axlowdimlem14  28213  axlowdim  28219  axcontlem5  28226  axcontlem7  28228  nb3grprlem2  28638  cplgr3v  28692  cusgrsizeindslem  28708  sizusglecusglem2  28719  umgr2v2e  28782  cusgrrusgr  28838  iswlk  28867  edginwlk  28892  uspgr2wlkeq  28903  uspgr2wlkeq2  28904  uspgr2wlkeqi  28905  wlkonprop  28915  wlkon2n0  28923  pthdadjvtx  28987  upgr2pthnlp  28989  spthonepeq  29009  pthdlem2lem  29024  crctcshwlkn0lem3  29066  crctcshwlkn0lem5  29068  wlkiswwlks2lem4  29126  wlkiswwlks2lem6  29128  wlklnwwlkln2lem  29136  wwlksnred  29146  wwlksnextbi  29148  wwlksnextwrd  29151  2pthdlem1  29184  2wlkdlem10  29189  umgr2adedgwlkonALT  29201  elwwlks2s3  29205  elwwlks2ons3im  29208  s3wwlks2on  29210  2wspdisj  29216  2wspiundisj  29217  clwwlkgt0  29239  clwlkclwwlklem2a4  29250  clwlkclwwlklem2a  29251  clwlkclwwlk  29255  clwlkclwwlk2  29256  clwlkclwwlkfo  29262  clwwisshclwwslemlem  29266  erclwwlktr  29275  clwwlkf  29300  wwlksubclwwlk  29311  erclwwlkntr  29324  clwwlknon  29343  frcond1  29519  frgr3v  29528  3vfriswmgr  29531  frgrwopreglem4a  29563  frrusgrord0lem  29592  clwwnonrepclwwnon  29598  extwwlkfab  29605  numclwwlk1lem2f1  29610  numclwwlk1lem2fo  29611  clwlknon2num  29621  numclwwlk2lem1  29629  numclwlk2lem2f  29630  numclwlk2lem2f1o  29632  numclwwlk2  29634  frgrreggt1  29646  friendshipgt3  29651  imsmetlem  29943  nmoxr  30019  nmoolb  30024  blometi  30056  phpar2  30076  phpar  30077  ipasslem5  30088  hvadd32  30287  hvaddsub12  30291  hvaddsubass  30294  hvsubass  30297  hvsub32  30298  hvsubdistr1  30302  hvsubdistr2  30303  hvmulcan  30325  hvmulcan2  30326  hvsubcan  30327  his5  30339  his2sub  30345  hhssabloilem  30514  hhssnv  30517  shlej2  30614  pjoi0  30970  hodcl  31000  hoadd32  31036  hosubdi  31061  hosubsub2  31065  hoaddsubass  31068  hosubsub4  31071  nmoplb  31160  unop  31168  hmop  31175  nmfnlb  31177  lnopmul  31220  kbass1  31369  kbass2  31370  leopmul2i  31388  leoptr  31390  cvntr  31545  mdslmd4i  31586  mdexchi  31588  atcv1  31633  sumdmdii  31668  fcoinvbr  31836  fpwrelmapffs  31959  xreceu  32088  isinftm  32327  unitdivcld  32881  esummulc1  33079  hasheuni  33083  unelsiga  33132  inelpisys  33152  carsgsigalem  33314  signswmnd  33568  bnj545  33906  bnj594  33923  bnj1311  34035  fineqvac  34097  hashf1dmcdm  34105  usgrgt2cycl  34121  subgrwlk  34123  acycgr1v  34140  cvmsf1o  34263  cvmscld  34264  satefvfmla1  34416  elnanelprv  34420  lediv2aALT  34662  gcd32  34719  fununiq  34740  dfrdg4  34923  brcolinear  35031  colinearex  35032  nn0prpwlem  35207  clsun  35213  fnemeet1  35251  fnemeet2  35252  fnejoin1  35253  fnejoin2  35254  eltail  35259  rdgeqoa  36251  nlpineqsn  36289  curf  36466  lindsadd  36481  poimirlem28  36516  cnambfre  36536  ftc1anclem4  36564  cocanfo  36587  f1ocan1fv  36594  metf1o  36623  ismtybnd  36675  ghomco  36759  isdrngo2  36826  inidl  36898  igenmin  36932  brxrn  37244  brredunds  37496  cmtvalN  38081  cvrval  38139  pmapmeet  38644  paddval  38669  paddssat  38685  elpcliN  38764  pclssN  38765  pclunN  38769  paddunN  38798  poldmj1N  38799  tendoplcl2  39649  tendoplcl  39652  dihmeet  40214  lcmineqlem1  40894  factwoffsmonot  41023  expgcd  41225  zexpgcd  41227  reltsub1  41259  reltsubadd2  41260  resubsub4  41262  reppncan  41266  resubdi  41269  readdcan2  41285  subresre  41303  mapco2g  41452  mzpcompact2lem  41489  eqrabdioph  41515  lerabdioph  41543  eluzrabdioph  41544  ltrabdioph  41546  nerabdioph  41547  dvdsrabdioph  41548  reglogcl  41628  rmxyadd  41660  rmyabs  41697  congadd  41705  congabseq  41713  rmydioph  41753  mendring  41934  mendlmod  41935  iocinico  41961  omge1  42047  relexp0a  42467  relexpaddss  42469  brcoffn  42781  ismnushort  43060  dvconstbi  43093  uzwo4  43740  ssin0  43742  ssinc  43776  ssdec  43777  fvmpt2bd  43866  disjf1o  43889  ssnnf1octb  43893  sub31  44000  fperiodmullem  44013  ssfiunibd  44019  infxr  44077  fmul01  44296  islptre  44335  lptre2pt  44356  limcleqr  44360  limclner  44367  limsuppnflem  44426  limsupvaluz2  44454  supcnvlimsup  44456  xlimmnfvlem2  44549  xlimmnfv  44550  xlimpnfvlem2  44553  xlimpnfv  44554  climxlim2lem  44561  coskpi2  44582  cosknegpi  44585  dvnmptdivc  44654  dvdsn1add  44655  dvnmptconst  44657  dvmptfprod  44661  dvnprodlem1  44662  dvnprodlem2  44663  ovolsplit  44704  stoweidlem60  44776  stowei  44780  dirkeritg  44818  fourierdlem70  44892  fourierdlem71  44893  fourierdlem103  44925  fourierdlem104  44926  fouriersw  44947  rrxtopnfi  45003  saluncl  45033  salexct  45050  sge0ltfirp  45116  sge0iunmpt  45134  meadjiunlem  45181  meaiuninc3v  45200  carageniuncllem1  45237  caratheodorylem1  45242  ovncvrrp  45280  ovnsubaddlem1  45286  hspmbllem2  45343  ovolval5lem3  45370  smfpimbor1lem1  45514  smfsuplem1  45527  smflimsuplem4  45539  sigarls  45573  cnambpcma  46002  elfzelfzlble  46029  fzoopth  46035  m1mod0mod1  46037  fsumsplitsndif  46041  fundcmpsurinjALT  46080  iccpartiltu  46090  prproropf1olem2  46172  fmtno4prmfac  46240  2pwp1prmfmtno  46258  lighneallem4b  46277  mogoldbblem  46388  gbegt5  46429  sbgoldbm  46452  nnsum3primesle9  46462  nnsum4primesodd  46464  nnsum4primesoddALTV  46465  evengpoap3  46467  nnsum4primesevenALTV  46469  isomgrtr  46507  strisomgrop  46508  isupwlk  46514  subrngmre  46741  rnglidlmmgm  46756  lidldomnnring  46828  2zrngacmnd  46840  rhmsubclem2  46985  rhmsubcALTVlem2  47003  fprmappr  47021  zlmodzxzscm  47033  gsumlsscl  47059  lincvalsng  47097  lincvalpr  47099  lincdifsn  47105  linc1  47106  lincellss  47107  difmodm1lt  47208  fdivmpt  47226  digexp  47293  2arymaptfo  47340  line  47418  rrxline  47420  itsclc0xyqsolr  47455  iscnrm3r  47581  amgmwlem  47849