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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1089

This theorem is referenced by:  3ad2ant2  1134  3ad2ant3  1135  3simpc  1150  eupickb  2631  spc3egv  3593  sbciegft  3814  reuhyp  5417  predtrss  6320  onunel  6466  funopg  6579  funprg  6599  funtpg  6600  funcnvtp  6608  unima  6963  fvun1  6979  fnreseql  7046  xpprsng  7134  ftpg  7150  f13dfv  7268  f1ofvswap  7300  mpoeq3ia  7483  ordunel  7811  fex2  7920  funexw  7934  poxp  8110  poxp2  8125  poxp3  8132  poseq  8140  suppval1  8148  wfr3g  8303  smores3  8349  oaord  8543  oacan  8544  oaword  8545  omord  8564  omcan  8565  omwordri  8568  odi  8575  omass  8576  oeord  8584  oecan  8585  oewordri  8588  oeordsuc  8590  nnaord  8615  nnaordr  8616  nndi  8619  nnmass  8620  nnaword  8623  nnmord  8628  nnmwordri  8632  naddelim  8681  naddel1  8682  naddel2  8683  naddss1  8684  naddss2  8685  naddasslem2  8690  nadd32  8692  erov  8804  ecopovtrn  8810  ixpf  8910  f1oen4g  8956  f1dom4g  8957  mapxpen  9139  dif1enlemOLD  9153  ssfi  9169  sbthfilem  9197  sbthfi  9198  onomeneq  9224  fimax2g  9285  unbnn  9295  funisfsupp  9363  inelfi  9409  elfiun  9421  sup0  9457  suppr  9462  infpr  9494  ttrclss  9711  frr3g  9747  r111  9766  dif1card  10001  ackbij1lem16  10226  cff1  10249  cfflb  10250  cfsmolem  10261  fin23lem34  10337  hsmexlem2  10418  axcc3  10429  domtriomlem  10433  axdc3lem4  10444  axdc4lem  10446  axcclem  10448  konigthlem  10559  gchdomtri  10620  tskpr  10761  tskop  10762  tskuni  10774  tskun  10777  gruop  10796  gruun  10797  grudomon  10808  adderpqlem  10945  mulerpqlem  10946  addassnq  10949  mulassnq  10950  distrnq  10952  ltsonq  10960  ltanq  10962  ltmnq  10963  genpass  11000  distrlem1pr  11016  distrlem4pr  11017  ltsopr  11023  adddir  11201  axlttrn  11282  ltletr  11302  letr  11304  mul32  11376  mul31  11377  add32  11428  subsub23  11461  addsubass  11466  subcan2  11481  subsub2  11484  nppcan2  11487  sub32  11490  nnncan  11491  nnncan2  11493  pnpcan2  11496  subdi  11643  subdir  11644  receu  11855  mulcan1g  11863  mulcan2g  11864  divmul3  11873  divrec  11884  divrec2  11885  divsubdir  11904  subdivcomb2  11906  divdiv1  11921  redivcl  11929  div2neg  11933  ltmul2  12061  lemul1  12062  lemul2  12063  lemul2a  12065  lediv1  12075  gt0div  12076  ge0div  12077  mulsuble0b  12082  ltdivmul  12085  ledivmul  12086  ltdivmul2  12087  ledivmul2  12089  lemuldiv  12090  ltdiv23  12101  lediv23  12102  ledivp1i  12135  ltdivp1i  12136  uzind2  12651  nn0ind  12653  fnn0ind  12657  uz3m2nn  12871  xrltletr  13132  xrletr  13133  xrre2  13145  xrltmin  13157  xrlemin  13159  xleadd2a  13229  xleadd1  13230  xltadd2  13232  xmulasslem3  13261  xmulass  13262  xltmul2  13268  ixxdisj  13335  iooneg  13444  iccneg  13445  icoshft  13446  icoshftf1o  13447  icodisj  13449  snunioo  13451  fzen  13514  ssfzunsnext  13542  fzrev3  13563  2ffzeq  13618  fzoaddel2  13684  elfzodifsumelfzo  13694  ssfzoulel  13722  ssfzo12bi  13723  fzoshftral  13745  adddivflid  13779  flltdivnn0lt  13794  ltdifltdiv  13795  fldiv4p1lem1div2  13796  modcyc  13867  modcyc2  13868  modaddabs  13870  modsubmodmod  13891  modaddmodup  13895  modaddmulmod  13899  moddi  13900  modsubdir  13901  expdiv  14075  digit2  14195  nfile  14315  hashdifpr  14371  hashgt23el  14380  hashreshashfun  14395  fi1uzind  14454  ccatval1  14523  ccatass  14534  swrdval  14589  swrdnd  14600  swrd0  14604  swrdfv2  14607  pfxsuff1eqwrdeq  14645  swrdswrdlem  14650  pfxccatin12lem2a  14673  pfxccatin12lem1  14674  repswccat  14732  cshwidxmod  14749  cshwidxmodr  14750  cshf1  14756  repswcshw  14758  2cshw  14759  2cshwcom  14762  2cshwcshw  14772  cshwcsh2id  14775  ccatco  14782  2swrd2eqwrdeq  14900  wwlktovf  14903  brcnvtrclfv  14946  shftval2  15018  mulre  15064  absdiv  15238  absdiflt  15260  absdifle  15261  abs3dif  15274  cau3  15298  ello12r  15457  elo12r  15468  modfsummods  15735  geoisum1c  15822  rpnnen2lem4  16156  rpnnen2lem7  16159  dvdsmulc  16223  dvdsmulcr  16225  dvdsmultr1  16235  dvdsmultr2  16237  dvdssub2  16240  oexpneg  16284  divalgb  16343  ndvdsadd  16349  sadass  16408  modgcd  16470  dvdsgcd  16482  dvdsgcdb  16483  gcdass  16485  mulgcd  16486  absmulgcd  16487  rpmulgcd  16494  nn0seqcvgd  16503  algcvga  16512  lcmdvdsb  16546  lcmass  16547  lcmfunsnlem1  16570  lcmfunsnlem2lem1  16571  lcmfunsnlem2lem2  16572  coprmdvds  16586  coprmdvds2  16587  rpmul  16592  cncongr1  16600  cncongr2  16601  qnumdenbi  16676  modprm0  16734  coprimeprodsq  16737  pythagtriplem4  16748  pythagtriplem8  16752  pythagtriplem9  16753  pythagtriplem12  16755  pythagtriplem14  16757  pythagtriplem16  16759  pcpremul  16772  pcgcd  16807  vdwapval  16902  vdwapun  16903  prmgaplem3  16982  prmgaplem4  16983  prmgaplem7  16986  prmgapprmolem  16990  mreiincl  17536  mreincl  17539  mremre  17544  mrcss  17556  catcisolem  18056  pleval2  18286  pospo  18294  latlem  18386  latjcom  18396  latmcom  18412  lubss  18462  lubun  18464  clatglbss  18468  ipole  18483  ipolt  18484  pslem  18521  dirtr  18551  gsumsgrpccat  18717  gsumws2  18719  frmdmnd  18736  symggrplem  18761  isgrpi  18841  grpsubrcan  18900  grpinvsub  18901  grpsubeq0  18905  grpsubadd0sub  18906  grpnpcan  18911  qussub  19064  ghmsub  19094  symgpssefmnd  19257  symggrp  19262  symgextsymg  19286  gsmsymgreqlem2  19293  symgfixfolem1  19300  pmtrprfv3  19316  symggen  19332  lsmass  19531  efgsrel  19596  cntzcmn  19702  dvrcl  20210  unitdvcl  20211  dvrcan1  20215  subrgmre  20380  abvsubtri  20435  abvtrivd  20440  lmodvsubval2  20519  rmodislmodlem  20531  rmodislmod  20532  rmodislmodOLD  20533  lss0cl  20549  lssintcl  20567  lssincl  20568  reslmhm2  20656  lspvadd  20699  lspsntrim  20701  islbs3  20760  rrgeq0  20898  cncrng  20958  xrsmcmn  20960  cndrng  20966  cnsrng  20971  xrs1mnd  20975  absabv  20994  psgnco  21127  zrhpsgninv  21129  zrhpsgnevpm  21135  zrhpsgnodpm  21136  zrhpsgnelbas  21138  zrhcopsgnelbas  21139  uvcresum  21339  lindfmm  21373  lindsmm  21374  evlsval2  21641  mamudm  21881  mamufacex  21882  matsubgcell  21927  matsc  21943  scmatscmide  22000  scmatrhmcl  22021  1marepvsma1  22076  m1detdiag  22090  mdetralt  22101  m2detleiblem7  22120  gsummatr01lem3  22150  gsummatr01  22152  smadiadetlem0  22154  decpmate  22259  decpmatcl  22260  pm2mpcl  22290  pm2mpghmlem2  22305  chfacfscmul0  22351  chfacfscmulgsum  22353  chfacfpmmul0  22355  chfacfpmmulgsum  22357  unopn  22396  clsss  22549  cldmre  22573  toponmre  22588  opnssneib  22610  restabs  22660  restcls  22676  restntr  22677  hausnei2  22848  cmpsublem  22894  bwth  22905  hausmapdom  22995  ptpjcn  23106  upxp  23118  ptrescn  23134  xkopjcn  23151  fbssfi  23332  snfil  23359  ufprim  23404  rnelfm  23448  flimrest  23478  fclsrest  23519  tmdgsum  23590  blpnfctr  23933  mscl  23958  xmscl  23959  xmsge0  23960  xmseq0  23961  restmetu  24070  ngpds  24104  tngngp3  24164  unitnmn0  24176  xrsxmet  24316  metds0  24357  cncfmptc  24419  isclmp  24604  cnlmod  24647  ncvsi  24659  cphsqrtcl  24692  cfil3i  24777  cfilres  24804  cmssmscld  24858  cmmbl  25042  voliunlem2  25059  itg2ub  25242  itgrecl  25306  tdeglem3OLD  25567  r1pid  25668  eflogeq  26101  cxpadd  26178  cxpcom  26236  logbchbase  26265  relogbreexp  26269  relogbzexp  26270  relogbmulexp  26272  logbleb  26277  logblt  26278  lawcos  26310  pythag  26311  asinsinb  26391  acoscosb  26392  atantanb  26418  amgmlem  26483  lgsneg  26813  lgsne0  26827  lgsmodeq  26834  lgsmulsqcoprm  26835  gausslemma2dlem1a  26857  2sqreulem2  26944  sltres  27154  noetainflem1  27229  sltletr  27248  sletr  27250  nocvxmin  27269  madebdaylemold  27381  lrrecpo  27414  sltadd2im  27458  sleadd1im  27459  sleadd2im  27460  sleadd1  27461  sleadd2  27462  sltadd1  27464  addscan2  27465  addscan1  27466  subadds  27527  sltsub1  27532  divscl  27658  brbtwn2  28152  colinearalg  28157  eleesubd  28159  axcgrrflx  28161  axcgrtr  28162  axsegcon  28174  ax5seglem1  28175  ax5seglem2  28176  ax5seglem4  28179  axbtwnid  28186  axlowdimlem14  28202  axlowdim  28208  axcontlem5  28215  axcontlem7  28217  nb3grprlem2  28627  cplgr3v  28681  cusgrsizeindslem  28697  sizusglecusglem2  28708  umgr2v2e  28771  cusgrrusgr  28827  iswlk  28856  edginwlk  28881  uspgr2wlkeq  28892  uspgr2wlkeq2  28893  uspgr2wlkeqi  28894  wlkonprop  28904  wlkon2n0  28912  pthdadjvtx  28976  upgr2pthnlp  28978  spthonepeq  28998  pthdlem2lem  29013  crctcshwlkn0lem3  29055  crctcshwlkn0lem5  29057  wlkiswwlks2lem4  29115  wlkiswwlks2lem6  29117  wlklnwwlkln2lem  29125  wwlksnred  29135  wwlksnextbi  29137  wwlksnextwrd  29140  2pthdlem1  29173  2wlkdlem10  29178  umgr2adedgwlkonALT  29190  elwwlks2s3  29194  elwwlks2ons3im  29197  s3wwlks2on  29199  2wspdisj  29205  2wspiundisj  29206  clwwlkgt0  29228  clwlkclwwlklem2a4  29239  clwlkclwwlklem2a  29240  clwlkclwwlk  29244  clwlkclwwlk2  29245  clwlkclwwlkfo  29251  clwwisshclwwslemlem  29255  erclwwlktr  29264  clwwlkf  29289  wwlksubclwwlk  29300  erclwwlkntr  29313  clwwlknon  29332  frcond1  29508  frgr3v  29517  3vfriswmgr  29520  frgrwopreglem4a  29552  frrusgrord0lem  29581  clwwnonrepclwwnon  29587  extwwlkfab  29594  numclwwlk1lem2f1  29599  numclwwlk1lem2fo  29600  clwlknon2num  29610  numclwwlk2lem1  29618  numclwlk2lem2f  29619  numclwlk2lem2f1o  29621  numclwwlk2  29623  frgrreggt1  29635  friendshipgt3  29640  imsmetlem  29930  nmoxr  30006  nmoolb  30011  blometi  30043  phpar2  30063  phpar  30064  ipasslem5  30075  hvadd32  30274  hvaddsub12  30278  hvaddsubass  30281  hvsubass  30284  hvsub32  30285  hvsubdistr1  30289  hvsubdistr2  30290  hvmulcan  30312  hvmulcan2  30313  hvsubcan  30314  his5  30326  his2sub  30332  hhssabloilem  30501  hhssnv  30504  shlej2  30601  pjoi0  30957  hodcl  30987  hoadd32  31023  hosubdi  31048  hosubsub2  31052  hoaddsubass  31055  hosubsub4  31058  nmoplb  31147  unop  31155  hmop  31162  nmfnlb  31164  lnopmul  31207  kbass1  31356  kbass2  31357  leopmul2i  31375  leoptr  31377  cvntr  31532  mdslmd4i  31573  mdexchi  31575  atcv1  31620  sumdmdii  31655  fcoinvbr  31823  fpwrelmapffs  31946  xreceu  32075  isinftm  32314  unitdivcld  32869  esummulc1  33067  hasheuni  33071  unelsiga  33120  inelpisys  33140  carsgsigalem  33302  signswmnd  33556  bnj545  33894  bnj594  33911  bnj1311  34023  fineqvac  34085  hashf1dmcdm  34093  usgrgt2cycl  34109  subgrwlk  34111  acycgr1v  34128  cvmsf1o  34251  cvmscld  34252  satefvfmla1  34404  elnanelprv  34408  lediv2aALT  34650  gcd32  34707  fununiq  34728  dfrdg4  34911  brcolinear  35019  colinearex  35020  nn0prpwlem  35195  clsun  35201  fnemeet1  35239  fnemeet2  35240  fnejoin1  35241  fnejoin2  35242  eltail  35247  rdgeqoa  36239  nlpineqsn  36277  curf  36454  lindsadd  36469  poimirlem28  36504  cnambfre  36524  ftc1anclem4  36552  cocanfo  36575  f1ocan1fv  36582  metf1o  36611  ismtybnd  36663  ghomco  36747  isdrngo2  36814  inidl  36886  igenmin  36920  brxrn  37232  brredunds  37484  cmtvalN  38069  cvrval  38127  pmapmeet  38632  paddval  38657  paddssat  38673  elpcliN  38752  pclssN  38753  pclunN  38757  paddunN  38786  poldmj1N  38787  tendoplcl2  39637  tendoplcl  39640  dihmeet  40202  lcmineqlem1  40882  factwoffsmonot  41011  expgcd  41220  zexpgcd  41222  reltsub1  41255  reltsubadd2  41256  resubsub4  41258  reppncan  41262  resubdi  41265  readdcan2  41281  subresre  41299  mapco2g  41437  mzpcompact2lem  41474  eqrabdioph  41500  lerabdioph  41528  eluzrabdioph  41529  ltrabdioph  41531  nerabdioph  41532  dvdsrabdioph  41533  reglogcl  41613  rmxyadd  41645  rmyabs  41682  congadd  41690  congabseq  41698  rmydioph  41738  mendring  41919  mendlmod  41920  iocinico  41946  omge1  42032  relexp0a  42452  relexpaddss  42454  brcoffn  42766  ismnushort  43045  dvconstbi  43078  uzwo4  43725  ssin0  43727  ssinc  43761  ssdec  43762  fvmpt2bd  43851  disjf1o  43874  ssnnf1octb  43878  sub31  43986  fperiodmullem  43999  ssfiunibd  44005  infxr  44063  fmul01  44282  islptre  44321  lptre2pt  44342  limcleqr  44346  limclner  44353  limsuppnflem  44412  limsupvaluz2  44440  supcnvlimsup  44442  xlimmnfvlem2  44535  xlimmnfv  44536  xlimpnfvlem2  44539  xlimpnfv  44540  climxlim2lem  44547  coskpi2  44568  cosknegpi  44571  dvnmptdivc  44640  dvdsn1add  44641  dvnmptconst  44643  dvmptfprod  44647  dvnprodlem1  44648  dvnprodlem2  44649  ovolsplit  44690  stoweidlem60  44762  stowei  44766  dirkeritg  44804  fourierdlem70  44878  fourierdlem71  44879  fourierdlem103  44911  fourierdlem104  44912  fouriersw  44933  rrxtopnfi  44989  saluncl  45019  salexct  45036  sge0ltfirp  45102  sge0iunmpt  45120  meadjiunlem  45167  meaiuninc3v  45186  carageniuncllem1  45223  caratheodorylem1  45228  ovncvrrp  45266  ovnsubaddlem1  45272  hspmbllem2  45329  ovolval5lem3  45356  smfpimbor1lem1  45500  smfsuplem1  45513  smflimsuplem4  45525  sigarls  45559  cnambpcma  45988  elfzelfzlble  46015  fzoopth  46021  m1mod0mod1  46023  fsumsplitsndif  46027  fundcmpsurinjALT  46066  iccpartiltu  46076  prproropf1olem2  46158  fmtno4prmfac  46226  2pwp1prmfmtno  46244  lighneallem4b  46263  mogoldbblem  46374  gbegt5  46415  sbgoldbm  46438  nnsum3primesle9  46448  nnsum4primesodd  46450  nnsum4primesoddALTV  46451  evengpoap3  46453  nnsum4primesevenALTV  46455  isomgrtr  46493  strisomgrop  46494  isupwlk  46500  subrngmre  46725  rnglidlmmgm  46738  lidldomnnring  46781  2zrngacmnd  46793  rhmsubclem2  46938  rhmsubcALTVlem2  46956  fprmappr  46974  zlmodzxzscm  46986  gsumlsscl  47012  lincvalsng  47050  lincvalpr  47052  lincdifsn  47058  linc1  47059  lincellss  47060  difmodm1lt  47161  fdivmpt  47179  digexp  47246  2arymaptfo  47293  line  47371  rrxline  47373  itsclc0xyqsolr  47408  iscnrm3r  47534  amgmwlem  47802