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  2635  spc3egv  3562  sbciegft  3777  reuhyp  5375  predtrss  6276  onunel  6422  funopg  6535  funprg  6555  funtpg  6556  funcnvtp  6564  unima  6916  fvun1  6932  fnreseql  6998  xpprsng  7086  ftpg  7102  f13dfv  7220  f1ofvswap  7252  mpoeq3ia  7435  ordunel  7762  fex2  7870  funexw  7884  poxp  8060  poxp2  8075  poxp3  8082  poseq  8090  suppval1  8098  wfr3g  8253  smores3  8299  oaord  8494  oacan  8495  oaword  8496  omord  8515  omcan  8516  omwordri  8519  odi  8526  omass  8527  oeord  8535  oecan  8536  oewordri  8539  oeordsuc  8541  nnaord  8566  nnaordr  8567  nndi  8570  nnmass  8571  nnaword  8574  nnmord  8579  nnmwordri  8583  naddelim  8631  naddel1  8632  naddel2  8633  naddss1  8634  naddss2  8635  naddasslem2  8639  nadd32  8641  erov  8753  ecopovtrn  8759  ixpf  8858  f1oen4g  8904  f1dom4g  8905  mapxpen  9087  dif1enlemOLD  9101  ssfi  9117  sbthfilem  9145  sbthfi  9146  onomeneq  9172  fimax2g  9233  unbnn  9243  funisfsupp  9310  inelfi  9354  elfiun  9366  sup0  9402  suppr  9407  infpr  9439  ttrclss  9656  frr3g  9692  r111  9711  dif1card  9946  ackbij1lem16  10171  cff1  10194  cfflb  10195  cfsmolem  10206  fin23lem34  10282  hsmexlem2  10363  axcc3  10374  domtriomlem  10378  axdc3lem4  10389  axdc4lem  10391  axcclem  10393  konigthlem  10504  gchdomtri  10565  tskpr  10706  tskop  10707  tskuni  10719  tskun  10722  gruop  10741  gruun  10742  grudomon  10753  adderpqlem  10890  mulerpqlem  10891  addassnq  10894  mulassnq  10895  distrnq  10897  ltsonq  10905  ltanq  10907  ltmnq  10908  genpass  10945  distrlem1pr  10961  distrlem4pr  10962  ltsopr  10968  adddir  11146  axlttrn  11227  ltletr  11247  letr  11249  mul32  11321  mul31  11322  add32  11373  subsub23  11406  addsubass  11411  subcan2  11426  subsub2  11429  nppcan2  11432  sub32  11435  nnncan  11436  nnncan2  11438  pnpcan2  11441  subdi  11588  subdir  11589  receu  11800  mulcan1g  11808  mulcan2g  11809  divmul3  11818  divrec  11829  divrec2  11830  divsubdir  11849  subdivcomb2  11851  divdiv1  11866  redivcl  11874  div2neg  11878  ltmul2  12006  lemul1  12007  lemul2  12008  lemul2a  12010  lediv1  12020  gt0div  12021  ge0div  12022  mulsuble0b  12027  ltdivmul  12030  ledivmul  12031  ltdivmul2  12032  ledivmul2  12034  lemuldiv  12035  ltdiv23  12046  lediv23  12047  ledivp1i  12080  ltdivp1i  12081  uzind2  12596  nn0ind  12598  fnn0ind  12602  uz3m2nn  12816  xrltletr  13076  xrletr  13077  xrre2  13089  xrltmin  13101  xrlemin  13103  xleadd2a  13173  xleadd1  13174  xltadd2  13176  xmulasslem3  13205  xmulass  13206  xltmul2  13212  ixxdisj  13279  iooneg  13388  iccneg  13389  icoshft  13390  icoshftf1o  13391  icodisj  13393  snunioo  13395  fzen  13458  ssfzunsnext  13486  fzrev3  13507  2ffzeq  13562  fzoaddel2  13628  elfzodifsumelfzo  13638  ssfzoulel  13666  ssfzo12bi  13667  fzoshftral  13689  adddivflid  13723  flltdivnn0lt  13738  ltdifltdiv  13739  fldiv4p1lem1div2  13740  modcyc  13811  modcyc2  13812  modaddabs  13814  modsubmodmod  13835  modaddmodup  13839  modaddmulmod  13843  moddi  13844  modsubdir  13845  expdiv  14019  digit2  14139  nfile  14259  hashdifpr  14315  hashgt23el  14324  hashreshashfun  14339  fi1uzind  14396  ccatval1  14465  ccatass  14476  swrdval  14531  swrdnd  14542  swrd0  14546  swrdfv2  14549  pfxsuff1eqwrdeq  14587  swrdswrdlem  14592  pfxccatin12lem2a  14615  pfxccatin12lem1  14616  repswccat  14674  cshwidxmod  14691  cshwidxmodr  14692  cshf1  14698  repswcshw  14700  2cshw  14701  2cshwcom  14704  2cshwcshw  14714  cshwcsh2id  14717  ccatco  14724  2swrd2eqwrdeq  14842  wwlktovf  14845  brcnvtrclfv  14888  shftval2  14960  mulre  15006  absdiv  15180  absdiflt  15202  absdifle  15203  abs3dif  15216  cau3  15240  ello12r  15399  elo12r  15410  modfsummods  15678  geoisum1c  15765  rpnnen2lem4  16099  rpnnen2lem7  16102  dvdsmulc  16166  dvdsmulcr  16168  dvdsmultr1  16178  dvdsmultr2  16180  dvdssub2  16183  oexpneg  16227  divalgb  16286  ndvdsadd  16292  sadass  16351  modgcd  16413  dvdsgcd  16425  dvdsgcdb  16426  gcdass  16428  mulgcd  16429  absmulgcd  16430  rpmulgcd  16437  nn0seqcvgd  16446  algcvga  16455  lcmdvdsb  16489  lcmass  16490  lcmfunsnlem1  16513  lcmfunsnlem2lem1  16514  lcmfunsnlem2lem2  16515  coprmdvds  16529  coprmdvds2  16530  rpmul  16535  cncongr1  16543  cncongr2  16544  qnumdenbi  16619  modprm0  16677  coprimeprodsq  16680  pythagtriplem4  16691  pythagtriplem8  16695  pythagtriplem9  16696  pythagtriplem12  16698  pythagtriplem14  16700  pythagtriplem16  16702  pcpremul  16715  pcgcd  16750  vdwapval  16845  vdwapun  16846  prmgaplem3  16925  prmgaplem4  16926  prmgaplem7  16929  prmgapprmolem  16933  mreiincl  17476  mreincl  17479  mremre  17484  mrcss  17496  catcisolem  17996  pleval2  18226  pospo  18234  latlem  18326  latjcom  18336  latmcom  18352  lubss  18402  lubun  18404  clatglbss  18408  ipole  18423  ipolt  18424  pslem  18461  dirtr  18491  gsumsgrpccat  18650  gsumws2  18652  frmdmnd  18669  symggrplem  18694  isgrpi  18773  grpsubrcan  18828  grpinvsub  18829  grpsubeq0  18833  grpsubadd0sub  18834  grpnpcan  18839  qussub  18990  ghmsub  19016  symgpssefmnd  19177  symggrp  19182  symgextsymg  19206  gsmsymgreqlem2  19213  symgfixfolem1  19220  pmtrprfv3  19236  symggen  19252  lsmass  19451  efgsrel  19516  cntzcmn  19618  dvrcl  20115  unitdvcl  20116  dvrcan1  20120  subrgmre  20246  abvsubtri  20294  abvtrivd  20299  lmodvsubval2  20377  rmodislmodlem  20389  rmodislmod  20390  rmodislmodOLD  20391  lss0cl  20407  lssintcl  20425  lssincl  20426  reslmhm2  20514  lspvadd  20557  lspsntrim  20559  islbs3  20616  rrgeq0  20760  cncrng  20818  xrsmcmn  20820  cndrng  20826  cnsrng  20831  xrs1mnd  20835  absabv  20854  psgnco  20987  zrhpsgninv  20989  zrhpsgnevpm  20995  zrhpsgnodpm  20996  zrhpsgnelbas  20998  zrhcopsgnelbas  20999  uvcresum  21199  lindfmm  21233  lindsmm  21234  evlsval2  21497  mamudm  21737  mamufacex  21738  matsubgcell  21783  matsc  21799  scmatscmide  21856  scmatrhmcl  21877  1marepvsma1  21932  m1detdiag  21946  mdetralt  21957  m2detleiblem7  21976  gsummatr01lem3  22006  gsummatr01  22008  smadiadetlem0  22010  decpmate  22115  decpmatcl  22116  pm2mpcl  22146  pm2mpghmlem2  22161  chfacfscmul0  22207  chfacfscmulgsum  22209  chfacfpmmul0  22211  chfacfpmmulgsum  22213  unopn  22252  clsss  22405  cldmre  22429  toponmre  22444  opnssneib  22466  restabs  22516  restcls  22532  restntr  22533  hausnei2  22704  cmpsublem  22750  bwth  22761  hausmapdom  22851  ptpjcn  22962  upxp  22974  ptrescn  22990  xkopjcn  23007  fbssfi  23188  snfil  23215  ufprim  23260  rnelfm  23304  flimrest  23334  fclsrest  23375  tmdgsum  23446  blpnfctr  23789  mscl  23814  xmscl  23815  xmsge0  23816  xmseq0  23817  restmetu  23926  ngpds  23960  tngngp3  24020  unitnmn0  24032  xrsxmet  24172  metds0  24213  cncfmptc  24275  isclmp  24460  cnlmod  24503  ncvsi  24515  cphsqrtcl  24548  cfil3i  24633  cfilres  24660  cmssmscld  24714  cmmbl  24898  voliunlem2  24915  itg2ub  25098  itgrecl  25162  tdeglem3OLD  25423  r1pid  25524  eflogeq  25957  cxpadd  26034  cxpcom  26092  logbchbase  26121  relogbreexp  26125  relogbzexp  26126  relogbmulexp  26128  logbleb  26133  logblt  26134  lawcos  26166  pythag  26167  asinsinb  26247  acoscosb  26248  atantanb  26274  amgmlem  26339  lgsneg  26669  lgsne0  26683  lgsmodeq  26690  lgsmulsqcoprm  26691  gausslemma2dlem1a  26713  2sqreulem2  26800  sltres  27010  noetainflem1  27085  sltletr  27104  sletr  27106  nocvxmin  27118  madebdaylemold  27227  lrrecpo  27253  sltadd2im  27295  sleadd1im  27296  sleadd2im  27297  sleadd1  27298  sleadd2  27299  sltadd1  27301  addscan2  27302  addscan1  27303  subadds  27357  sltsub1  27362  brbtwn2  27854  colinearalg  27859  eleesubd  27861  axcgrrflx  27863  axcgrtr  27864  axsegcon  27876  ax5seglem1  27877  ax5seglem2  27878  ax5seglem4  27881  axbtwnid  27888  axlowdimlem14  27904  axlowdim  27910  axcontlem5  27917  axcontlem7  27919  nb3grprlem2  28329  cplgr3v  28383  cusgrsizeindslem  28399  sizusglecusglem2  28410  umgr2v2e  28473  cusgrrusgr  28529  iswlk  28558  edginwlk  28583  uspgr2wlkeq  28594  uspgr2wlkeq2  28595  uspgr2wlkeqi  28596  wlkonprop  28606  wlkon2n0  28614  pthdadjvtx  28678  upgr2pthnlp  28680  spthonepeq  28700  pthdlem2lem  28715  crctcshwlkn0lem3  28757  crctcshwlkn0lem5  28759  wlkiswwlks2lem4  28817  wlkiswwlks2lem6  28819  wlklnwwlkln2lem  28827  wwlksnred  28837  wwlksnextbi  28839  wwlksnextwrd  28842  2pthdlem1  28875  2wlkdlem10  28880  umgr2adedgwlkonALT  28892  elwwlks2s3  28896  elwwlks2ons3im  28899  s3wwlks2on  28901  2wspdisj  28907  2wspiundisj  28908  clwwlkgt0  28930  clwlkclwwlklem2a4  28941  clwlkclwwlklem2a  28942  clwlkclwwlk  28946  clwlkclwwlk2  28947  clwlkclwwlkfo  28953  clwwisshclwwslemlem  28957  erclwwlktr  28966  clwwlkf  28991  wwlksubclwwlk  29002  erclwwlkntr  29015  clwwlknon  29034  frcond1  29210  frgr3v  29219  3vfriswmgr  29222  frgrwopreglem4a  29254  frrusgrord0lem  29283  clwwnonrepclwwnon  29289  extwwlkfab  29296  numclwwlk1lem2f1  29301  numclwwlk1lem2fo  29302  clwlknon2num  29312  numclwwlk2lem1  29320  numclwlk2lem2f  29321  numclwlk2lem2f1o  29323  numclwwlk2  29325  frgrreggt1  29337  friendshipgt3  29342  imsmetlem  29632  nmoxr  29708  nmoolb  29713  blometi  29745  phpar2  29765  phpar  29766  ipasslem5  29777  hvadd32  29976  hvaddsub12  29980  hvaddsubass  29983  hvsubass  29986  hvsub32  29987  hvsubdistr1  29991  hvsubdistr2  29992  hvmulcan  30014  hvmulcan2  30015  hvsubcan  30016  his5  30028  his2sub  30034  hhssabloilem  30203  hhssnv  30206  shlej2  30303  pjoi0  30659  hodcl  30689  hoadd32  30725  hosubdi  30750  hosubsub2  30754  hoaddsubass  30757  hosubsub4  30760  nmoplb  30849  unop  30857  hmop  30864  nmfnlb  30866  lnopmul  30909  kbass1  31058  kbass2  31059  leopmul2i  31077  leoptr  31079  cvntr  31234  mdslmd4i  31275  mdexchi  31277  atcv1  31322  sumdmdii  31357  fcoinvbr  31526  fpwrelmapffs  31651  xreceu  31778  isinftm  32017  unitdivcld  32482  esummulc1  32680  hasheuni  32684  unelsiga  32733  inelpisys  32753  carsgsigalem  32915  signswmnd  33169  bnj545  33507  bnj594  33524  bnj1311  33636  fineqvac  33698  hashf1dmcdm  33708  usgrgt2cycl  33724  subgrwlk  33726  acycgr1v  33743  cvmsf1o  33866  cvmscld  33867  satefvfmla1  34019  elnanelprv  34023  lediv2aALT  34265  gcd32  34322  fununiq  34343  dfrdg4  34536  brcolinear  34644  colinearex  34645  nn0prpwlem  34794  clsun  34800  fnemeet1  34838  fnemeet2  34839  fnejoin1  34840  fnejoin2  34841  eltail  34846  rdgeqoa  35841  nlpineqsn  35879  curf  36056  lindsadd  36071  poimirlem28  36106  cnambfre  36126  ftc1anclem4  36154  cocanfo  36177  f1ocan1fv  36185  metf1o  36214  ismtybnd  36266  ghomco  36350  isdrngo2  36417  inidl  36489  igenmin  36523  brxrn  36836  brredunds  37088  cmtvalN  37673  cvrval  37731  pmapmeet  38236  paddval  38261  paddssat  38277  elpcliN  38356  pclssN  38357  pclunN  38361  paddunN  38390  poldmj1N  38391  tendoplcl2  39241  tendoplcl  39244  dihmeet  39806  lcmineqlem1  40486  factwoffsmonot  40615  expgcd  40806  zexpgcd  40808  reltsub1  40841  reltsubadd2  40842  resubsub4  40844  reppncan  40848  resubdi  40851  readdcan2  40867  subresre  40885  mapco2g  41023  mzpcompact2lem  41060  eqrabdioph  41086  lerabdioph  41114  eluzrabdioph  41115  ltrabdioph  41117  nerabdioph  41118  dvdsrabdioph  41119  reglogcl  41199  rmxyadd  41231  rmyabs  41268  congadd  41276  congabseq  41284  rmydioph  41324  mendring  41505  mendlmod  41506  iocinico  41532  omge1  41617  relexp0a  41978  relexpaddss  41980  brcoffn  42292  ismnushort  42571  dvconstbi  42604  uzwo4  43251  ssin0  43253  ssinc  43287  ssdec  43288  fvmpt2bd  43377  disjf1o  43400  ssnnf1octb  43404  sub31  43514  fperiodmullem  43527  ssfiunibd  43533  infxr  43591  fmul01  43811  islptre  43850  lptre2pt  43871  limcleqr  43875  limclner  43882  limsuppnflem  43941  limsupvaluz2  43969  supcnvlimsup  43971  xlimmnfvlem2  44064  xlimmnfv  44065  xlimpnfvlem2  44068  xlimpnfv  44069  climxlim2lem  44076  coskpi2  44097  cosknegpi  44100  dvnmptdivc  44169  dvdsn1add  44170  dvnmptconst  44172  dvmptfprod  44176  dvnprodlem1  44177  dvnprodlem2  44178  ovolsplit  44219  stoweidlem60  44291  stowei  44295  dirkeritg  44333  fourierdlem70  44407  fourierdlem71  44408  fourierdlem103  44440  fourierdlem104  44441  fouriersw  44462  rrxtopnfi  44518  saluncl  44548  salexct  44565  sge0ltfirp  44631  sge0iunmpt  44649  meadjiunlem  44696  meaiuninc3v  44715  carageniuncllem1  44752  caratheodorylem1  44757  ovncvrrp  44795  ovnsubaddlem1  44801  hspmbllem2  44858  ovolval5lem3  44885  smfpimbor1lem1  45029  smfsuplem1  45042  smflimsuplem4  45054  sigarls  45088  cnambpcma  45516  elfzelfzlble  45543  fzoopth  45549  m1mod0mod1  45551  fsumsplitsndif  45555  fundcmpsurinjALT  45594  iccpartiltu  45604  prproropf1olem2  45686  fmtno4prmfac  45754  2pwp1prmfmtno  45772  lighneallem4b  45791  mogoldbblem  45902  gbegt5  45943  sbgoldbm  45966  nnsum3primesle9  45976  nnsum4primesodd  45978  nnsum4primesoddALTV  45979  evengpoap3  45981  nnsum4primesevenALTV  45983  isomgrtr  46021  strisomgrop  46022  isupwlk  46028  lidldomnnring  46218  2zrngacmnd  46230  rhmsubclem2  46375  rhmsubcALTVlem2  46393  fprmappr  46411  zlmodzxzscm  46423  gsumlsscl  46449  lincvalsng  46487  lincvalpr  46489  lincdifsn  46495  linc1  46496  lincellss  46497  difmodm1lt  46598  fdivmpt  46616  digexp  46683  2arymaptfo  46730  line  46808  rrxline  46810  itsclc0xyqsolr  46845  iscnrm3r  46971  amgmwlem  47239