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 713	. 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  1134  3ad2ant3  1135  3simpc  1150  eupickb  2638  spc3egv  3616  sbciegftOLD  3843  reuhyp  5438  predtrss  6354  onunel  6500  funopg  6612  funprg  6632  funtpg  6633  funcnvtp  6641  unima  6997  fvun1  7013  fnreseql  7081  xpprsng  7174  ftpg  7190  f13dfv  7310  f1ocoima  7339  f1ofvswap  7342  mpoeq3ia  7528  ordunel  7863  fex2  7974  funexw  7992  poxp  8169  poxp2  8184  poxp3  8191  poseq  8199  suppval1  8207  wfr3g  8363  smores3  8409  oaord  8603  oacan  8604  oaword  8605  omord  8624  omcan  8625  omwordri  8628  odi  8635  omass  8636  oeord  8644  oecan  8645  oewordri  8648  oeordsuc  8650  nnaord  8675  nnaordr  8676  nndi  8679  nnmass  8680  nnaword  8683  nnmord  8688  nnmwordri  8692  naddelim  8742  naddel1  8743  naddel2  8744  naddss1  8745  naddss2  8746  naddasslem2  8751  nadd32  8753  erov  8872  ecopovtrn  8878  ixpf  8978  f1oen4g  9024  f1dom4g  9025  mapxpen  9209  dif1enlemOLD  9223  ssfi  9240  sbthfilem  9264  sbthfi  9265  onomeneq  9291  fimax2g  9350  unbnn  9360  funisfsupp  9437  inelfi  9487  elfiun  9499  sup0  9535  suppr  9540  infpr  9572  ttrclss  9789  frr3g  9825  r111  9844  dif1card  10079  ackbij1lem16  10303  cff1  10327  cfflb  10328  cfsmolem  10339  fin23lem34  10415  hsmexlem2  10496  axcc3  10507  domtriomlem  10511  axdc3lem4  10522  axdc4lem  10524  axcclem  10526  konigthlem  10637  gchdomtri  10698  tskpr  10839  tskop  10840  tskuni  10852  tskun  10855  gruop  10874  gruun  10875  grudomon  10886  adderpqlem  11023  mulerpqlem  11024  addassnq  11027  mulassnq  11028  distrnq  11030  ltsonq  11038  ltanq  11040  ltmnq  11041  genpass  11078  distrlem1pr  11094  distrlem4pr  11095  ltsopr  11101  adddir  11281  axlttrn  11362  ltletr  11382  letr  11384  mul32  11456  mul31  11457  add32  11508  subsub23  11541  addsubass  11546  subcan2  11561  subsub2  11564  nppcan2  11567  sub32  11570  nnncan  11571  nnncan2  11573  pnpcan2  11576  subdi  11723  subdir  11724  receu  11935  mulcan1g  11943  mulcan2g  11944  divmul3  11954  divrec  11965  divrec2  11966  div11  11977  divsubdir  11988  subdivcomb2  11990  divdiv1  12005  redivcl  12013  div2neg  12017  ltmul2  12145  lemul1  12146  lemul2  12147  lemul2a  12149  lediv1  12160  gt0div  12161  ge0div  12162  mulsuble0b  12167  ltdivmul  12170  ledivmul  12171  ltdivmul2  12172  ledivmul2  12174  lemuldiv  12175  ltdiv23  12186  lediv23  12187  ledivp1i  12220  ltdivp1i  12221  uzind2  12736  nn0ind  12738  fnn0ind  12742  uz3m2nn  12956  xrltletr  13219  xrletr  13220  xrre2  13232  xrltmin  13244  xrlemin  13246  xleadd2a  13316  xleadd1  13317  xltadd2  13319  xmulasslem3  13348  xmulass  13349  xltmul2  13355  ixxdisj  13422  iooneg  13531  iccneg  13532  icoshft  13533  icoshftf1o  13534  icodisj  13536  snunioo  13538  fzen  13601  ssfzunsnext  13629  fzrev3  13650  2ffzeq  13706  fzoaddel2  13772  elfzodifsumelfzo  13782  ssfzoulel  13810  ssfzo12bi  13811  fzoopth  13812  fzoshftral  13834  adddivflid  13869  flltdivnn0lt  13884  ltdifltdiv  13885  fldiv4p1lem1div2  13886  modcyc  13957  modcyc2  13958  modaddabs  13960  modsubmodmod  13981  modaddmodup  13985  modaddmulmod  13989  moddi  13990  modsubdir  13991  expdiv  14164  digit2  14285  nfile  14408  hashdifpr  14464  hashgt23el  14473  hashreshashfun  14488  hashf1dmcdm  14493  hash3tpexb  14543  fi1uzind  14556  ccatval1  14625  ccatass  14636  swrdval  14691  swrdnd  14702  swrd0  14706  swrdfv2  14709  pfxsuff1eqwrdeq  14747  swrdswrdlem  14752  pfxccatin12lem2a  14775  pfxccatin12lem1  14776  repswccat  14834  cshwidxmod  14851  cshwidxmodr  14852  cshf1  14858  repswcshw  14860  2cshw  14861  2cshwcom  14864  2cshwcshw  14874  cshwcsh2id  14877  ccatco  14884  2swrd2eqwrdeq  15002  wwlktovf  15005  brcnvtrclfv  15052  shftval2  15124  mulre  15170  absdiv  15344  absdiflt  15366  absdifle  15367  abs3dif  15380  cau3  15404  ello12r  15563  elo12r  15574  modfsummods  15841  geoisum1c  15928  rpnnen2lem4  16265  rpnnen2lem7  16268  dvdsmulc  16332  dvdsmulcr  16334  dvdsmultr1  16344  dvdsmultr2  16346  dvdssub2  16349  oexpneg  16393  divalgb  16452  ndvdsadd  16458  sadass  16517  modgcd  16579  dvdsgcd  16591  dvdsgcdb  16592  gcdass  16594  mulgcd  16595  absmulgcd  16596  rpmulgcd  16604  expgcd  16610  zexpgcd  16612  nn0seqcvgd  16617  algcvga  16626  lcmdvdsb  16660  lcmass  16661  lcmfunsnlem1  16684  lcmfunsnlem2lem1  16685  lcmfunsnlem2lem2  16686  coprmdvds  16700  coprmdvds2  16701  rpmul  16706  cncongr1  16714  cncongr2  16715  qnumdenbi  16791  modprm0  16852  coprimeprodsq  16855  pythagtriplem4  16866  pythagtriplem8  16870  pythagtriplem9  16871  pythagtriplem12  16873  pythagtriplem14  16875  pythagtriplem16  16877  pcpremul  16890  pcgcd  16925  vdwapval  17020  vdwapun  17021  prmgaplem3  17100  prmgaplem4  17101  prmgaplem7  17104  prmgapprmolem  17108  mreiincl  17654  mreincl  17657  mremre  17662  mrcss  17674  catcisolem  18177  pleval2  18407  pospo  18415  latlem  18507  latjcom  18517  latmcom  18533  lubss  18583  lubun  18585  clatglbss  18589  ipole  18604  ipolt  18605  pslem  18642  dirtr  18672  gsumsgrpccat  18875  gsumws2  18877  frmdmnd  18894  symggrplem  18919  isgrpi  18999  grpsubrcan  19061  grpinvsub  19062  grpsubeq0  19066  grpsubadd0sub  19067  grpnpcan  19072  qussub  19231  ghmsub  19264  symgpssefmnd  19437  symggrp  19442  symgextsymg  19466  gsmsymgreqlem2  19473  symgfixfolem1  19480  pmtrprfv3  19496  symggen  19512  lsmass  19711  efgsrel  19776  cntzcmn  19882  dvrcl  20430  unitdvcl  20431  dvrcan1  20435  subrngmre  20588  subrgmre  20625  rhmsubclem2  20708  rrgeq0  20722  abvsubtri  20850  abvtrivd  20855  lmodvsubval2  20937  rmodislmodlem  20949  rmodislmod  20950  rmodislmodOLD  20951  lss0cl  20968  lssintcl  20985  lssincl  20986  reslmhm2  21075  lspvadd  21118  lspsntrim  21120  islbs3  21180  rnglidlmmgm  21278  cncrng  21424  cncrngOLD  21425  xrsmcmn  21427  cndrng  21434  cndrngOLD  21435  cnsrng  21441  xrs1mnd  21445  absabv  21465  psgnco  21624  zrhpsgninv  21626  zrhpsgnevpm  21632  zrhpsgnodpm  21633  zrhpsgnelbas  21635  zrhcopsgnelbas  21636  uvcresum  21836  lindfmm  21870  lindsmm  21871  evlsval2  22134  mamudm  22420  mamufacex  22421  matsubgcell  22461  matsc  22477  scmatscmide  22534  scmatrhmcl  22555  1marepvsma1  22610  m1detdiag  22624  mdetralt  22635  m2detleiblem7  22654  gsummatr01lem3  22684  gsummatr01  22686  smadiadetlem0  22688  decpmate  22793  decpmatcl  22794  pm2mpcl  22824  pm2mpghmlem2  22839  chfacfscmul0  22885  chfacfscmulgsum  22887  chfacfpmmul0  22889  chfacfpmmulgsum  22891  unopn  22930  clsss  23083  cldmre  23107  toponmre  23122  opnssneib  23144  restabs  23194  restcls  23210  restntr  23211  hausnei2  23382  cmpsublem  23428  bwth  23439  hausmapdom  23529  ptpjcn  23640  upxp  23652  ptrescn  23668  xkopjcn  23685  fbssfi  23866  snfil  23893  ufprim  23938  rnelfm  23982  flimrest  24012  fclsrest  24053  tmdgsum  24124  blpnfctr  24467  mscl  24492  xmscl  24493  xmsge0  24494  xmseq0  24495  restmetu  24604  ngpds  24638  tngngp3  24698  unitnmn0  24710  xrsxmet  24850  metds0  24891  mpomulcn  24910  cncfmptc  24957  isclmp  25149  cnlmod  25192  ncvsi  25204  cphsqrtcl  25237  cfil3i  25322  cfilres  25349  cmssmscld  25403  cmmbl  25588  voliunlem2  25605  itg2ub  25788  itgrecl  25853  r1pid  26220  eflogeq  26662  cxpadd  26739  cxpcom  26799  logbchbase  26832  relogbreexp  26836  relogbzexp  26837  relogbmulexp  26839  logbleb  26844  logblt  26845  lawcos  26877  pythag  26878  asinsinb  26958  acoscosb  26959  atantanb  26985  amgmlem  27051  lgsneg  27383  lgsne0  27397  lgsmodeq  27404  lgsmulsqcoprm  27405  gausslemma2dlem1a  27427  2sqreulem2  27514  sltres  27725  noetainflem1  27800  sltletr  27819  sletr  27821  nocvxmin  27841  madebdaylemold  27954  lrrecpo  27992  sltadd2im  28037  sleadd1im  28038  sleadd2im  28039  sleadd1  28040  sleadd2  28041  sltadd1  28043  addscan2  28044  addscan1  28045  subadds  28118  sltsub1  28124  divscl  28265  nohalf  28425  0reno  28447  brbtwn2  28938  colinearalg  28943  eleesubd  28945  axcgrrflx  28947  axcgrtr  28948  axsegcon  28960  ax5seglem1  28961  ax5seglem2  28962  ax5seglem4  28965  axbtwnid  28972  axlowdimlem14  28988  axlowdim  28994  axcontlem5  29001  axcontlem7  29003  nb3grprlem2  29416  cplgr3v  29470  cusgrsizeindslem  29487  sizusglecusglem2  29498  umgr2v2e  29561  cusgrrusgr  29617  iswlk  29646  edginwlk  29671  uspgr2wlkeq  29682  uspgr2wlkeq2  29683  uspgr2wlkeqi  29684  wlkonprop  29694  wlkon2n0  29702  pthdadjvtx  29766  upgr2pthnlp  29768  spthonepeq  29788  pthdlem2lem  29803  crctcshwlkn0lem3  29845  crctcshwlkn0lem5  29847  wlkiswwlks2lem4  29905  wlkiswwlks2lem6  29907  wlklnwwlkln2lem  29915  wwlksnred  29925  wwlksnextbi  29927  wwlksnextwrd  29930  2pthdlem1  29963  2wlkdlem10  29968  umgr2adedgwlkonALT  29980  elwwlks2s3  29984  elwwlks2ons3im  29987  s3wwlks2on  29989  2wspdisj  29995  2wspiundisj  29996  clwwlkgt0  30018  clwlkclwwlklem2a4  30029  clwlkclwwlklem2a  30030  clwlkclwwlk  30034  clwlkclwwlk2  30035  clwlkclwwlkfo  30041  clwwisshclwwslemlem  30045  erclwwlktr  30054  clwwlkf  30079  wwlksubclwwlk  30090  erclwwlkntr  30103  clwwlknon  30122  frcond1  30298  frgr3v  30307  3vfriswmgr  30310  frgrwopreglem4a  30342  frrusgrord0lem  30371  clwwnonrepclwwnon  30377  extwwlkfab  30384  numclwwlk1lem2f1  30389  numclwwlk1lem2fo  30390  clwlknon2num  30400  numclwwlk2lem1  30408  numclwlk2lem2f  30409  numclwlk2lem2f1o  30411  numclwwlk2  30413  frgrreggt1  30425  friendshipgt3  30430  imsmetlem  30722  nmoxr  30798  nmoolb  30803  blometi  30835  phpar2  30855  phpar  30856  ipasslem5  30867  hvadd32  31066  hvaddsub12  31070  hvaddsubass  31073  hvsubass  31076  hvsub32  31077  hvsubdistr1  31081  hvsubdistr2  31082  hvmulcan  31104  hvmulcan2  31105  hvsubcan  31106  his5  31118  his2sub  31124  hhssabloilem  31293  hhssnv  31296  shlej2  31393  pjoi0  31749  hodcl  31779  hoadd32  31815  hosubdi  31840  hosubsub2  31844  hoaddsubass  31847  hosubsub4  31850  nmoplb  31939  unop  31947  hmop  31954  nmfnlb  31956  lnopmul  31999  kbass1  32148  kbass2  32149  leopmul2i  32167  leoptr  32169  cvntr  32324  mdslmd4i  32365  mdexchi  32367  atcv1  32412  sumdmdii  32447  fcoinvbr  32627  fpwrelmapffs  32748  xreceu  32886  isinftm  33161  unitdivcld  33847  esummulc1  34045  hasheuni  34049  unelsiga  34098  inelpisys  34118  carsgsigalem  34280  signswmnd  34534  bnj545  34871  bnj594  34888  bnj1311  35000  fineqvac  35073  usgrgt2cycl  35098  subgrwlk  35100  acycgr1v  35117  cvmsf1o  35240  cvmscld  35241  satefvfmla1  35393  elnanelprv  35397  lediv2aALT  35645  gcd32  35711  fununiq  35732  dfrdg4  35915  brcolinear  36023  colinearex  36024  nn0prpwlem  36288  clsun  36294  fnemeet1  36332  fnemeet2  36333  fnejoin1  36334  fnejoin2  36335  eltail  36340  rdgeqoa  37336  nlpineqsn  37374  curf  37558  lindsadd  37573  poimirlem28  37608  cnambfre  37628  ftc1anclem4  37656  cocanfo  37679  f1ocan1fv  37686  metf1o  37715  ismtybnd  37767  ghomco  37851  isdrngo2  37918  inidl  37990  igenmin  38024  brxrn  38330  brredunds  38582  cmtvalN  39167  cvrval  39225  pmapmeet  39730  paddval  39755  paddssat  39771  elpcliN  39850  pclssN  39851  pclunN  39855  paddunN  39884  poldmj1N  39885  tendoplcl2  40735  tendoplcl  40738  dihmeet  41300  lcmineqlem1  41986  factwoffsmonot  42199  reltsub1  42362  reltsubadd2  42363  resubsub4  42365  reppncan  42369  resubdi  42372  readdcan2  42388  subresre  42406  mapco2g  42670  mzpcompact2lem  42707  eqrabdioph  42733  lerabdioph  42761  eluzrabdioph  42762  ltrabdioph  42764  nerabdioph  42765  dvdsrabdioph  42766  reglogcl  42846  rmxyadd  42878  rmyabs  42915  congadd  42923  congabseq  42931  rmydioph  42971  mendring  43149  mendlmod  43150  iocinico  43173  omge1  43259  relexp0a  43678  relexpaddss  43680  brcoffn  43992  ismnushort  44270  dvconstbi  44303  uzwo4  44955  ssin0  44957  ssinc  44989  ssdec  44990  fvmpt2bd  45077  disjf1o  45098  ssnnf1octb  45101  sub31  45205  fperiodmullem  45218  ssfiunibd  45224  infxr  45282  fmul01  45501  islptre  45540  lptre2pt  45561  limcleqr  45565  limclner  45572  limsuppnflem  45631  limsupvaluz2  45659  supcnvlimsup  45661  xlimmnfvlem2  45754  xlimmnfv  45755  xlimpnfvlem2  45758  xlimpnfv  45759  climxlim2lem  45766  coskpi2  45787  cosknegpi  45790  dvnmptdivc  45859  dvdsn1add  45860  dvnmptconst  45862  dvmptfprod  45866  dvnprodlem1  45867  dvnprodlem2  45868  ovolsplit  45909  stoweidlem60  45981  stowei  45985  dirkeritg  46023  fourierdlem70  46097  fourierdlem71  46098  fourierdlem103  46130  fourierdlem104  46131  fouriersw  46152  rrxtopnfi  46208  saluncl  46238  salexct  46255  sge0ltfirp  46321  sge0iunmpt  46339  meadjiunlem  46386  meaiuninc3v  46405  carageniuncllem1  46442  caratheodorylem1  46447  ovncvrrp  46485  ovnsubaddlem1  46491  hspmbllem2  46548  ovolval5lem3  46575  smfpimbor1lem1  46719  smfsuplem1  46732  smflimsuplem4  46744  sigarls  46778  cnambpcma  47209  elfzelfzlble  47236  m1mod0mod1  47243  fsumsplitsndif  47247  fundcmpsurinjALT  47286  iccpartiltu  47296  prproropf1olem2  47378  fmtno4prmfac  47446  2pwp1prmfmtno  47464  lighneallem4b  47483  mogoldbblem  47594  gbegt5  47635  sbgoldbm  47658  nnsum3primesle9  47668  nnsum4primesodd  47670  nnsum4primesoddALTV  47671  evengpoap3  47673  nnsum4primesevenALTV  47675  clnbgredg  47712  opstrgric  47779  clnbgrgrimlem  47785  grtrif1o  47793  isupwlk  47859  lidldomnnring  47959  2zrngacmnd  47971  rhmsubcALTVlem2  48005  fprmappr  48070  zlmodzxzscm  48082  gsumlsscl  48108  lincvalsng  48145  lincvalpr  48147  lincdifsn  48153  linc1  48154  lincellss  48155  difmodm1lt  48256  fdivmpt  48274  digexp  48341  2arymaptfo  48388  line  48466  rrxline  48468  itsclc0xyqsolr  48503  iscnrm3r  48628  amgmwlem  48896