Theorem 3adant1 1146

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  3ad2ant2  1150  3ad2ant3  1151  3simpc  1166  eupickb  2669  spc3egv  3571  reuhyp  5389  predtrss  6320  onunel  6465  funopg  6567  funprg  6587  funtpg  6588  funcnvtp  6596  unima  6954  fvun1  6970  fnreseql  7041  xpprsng  7134  ftpg  7151  f1ounsn  7268  f13dfv  7270  f1ocoima  7299  f1ofvswap  7302  mpoeq3ia  7486  ordunel  7819  fex2  7929  funexw  7945  poxp  8120  poxp2  8135  poxp3  8142  poseq  8150  suppval1  8158  wfr3g  8312  smores3  8336  oaord  8528  oacan  8529  oaword  8530  omord  8549  omcan  8550  omwordri  8553  odi  8560  omass  8561  oeord  8570  oecan  8571  oewordri  8574  oeordsuc  8576  nnaord  8601  nnaordr  8602  nndi  8605  nnmass  8606  nnaword  8609  nnmord  8614  nnmwordri  8618  naddelim  8669  naddel1  8670  naddel2  8671  naddss1  8672  naddss2  8673  naddasslem2  8678  nadd32  8680  erov  8808  ecopovtrn  8814  ixpf  8914  f1oen4g  8957  f1dom4g  8958  mapxpen  9127  ssfi  9153  sbthfilem  9178  sbthfi  9179  onomeneq  9194  fimax2g  9242  unbnn  9252  funisfsupp  9323  inelfi  9374  elfiun  9386  sup0  9423  suppr  9428  infpr  9461  ttrclss  9685  frr3g  9724  r111  9743  dif1card  9990  ackbij1lem16  10213  cff1  10238  cfflb  10239  cfsmolem  10250  fin23lem34  10326  hsmexlem2  10407  axcc3  10418  domtriomlem  10422  axdc3lem4  10433  axdc4lem  10435  axcclem  10437  konigthlem  10549  gchdomtri  10610  tskpr  10751  tskop  10752  tskuni  10764  tskun  10767  gruop  10786  gruun  10787  grudomon  10798  adderpqlem  10935  mulerpqlem  10936  addassnq  10939  mulassnq  10940  distrnq  10942  ltsonq  10950  ltanq  10952  ltmnq  10953  genpass  10990  distrlem1pr  11006  distrlem4pr  11007  ltsopr  11013  adddir  11193  axlttrn  11278  ltletr  11298  letr  11300  mul32  11372  mul31  11373  add32  11425  subsub23  11458  addsubass  11463  subcan2  11479  subsub2  11482  nppcan2  11485  sub32  11488  nnncan  11489  nnncan2  11491  pnpcan2  11494  subdi  11643  subdir  11644  receu  11855  mulcan1g  11863  mulcan2g  11864  divmul3  11873  divrec  11884  divrec2  11885  div11  11896  divsubdir  11904  subdivcomb2  11907  divdiv1  11922  redivcl  11930  div2neg  11934  ltmul2  12062  lemul1  12063  lemul2  12064  lemul2a  12066  lediv1  12076  gt0div  12077  ge0div  12078  mulsuble0b  12083  ltdivmul  12086  ledivmul  12087  ltdivmul2  12088  ledivmul2  12090  lemuldiv  12091  ltdiv23  12102  lediv23  12103  ledivp1i  12136  ltdivp1i  12137  uzind2  12685  nn0ind  12687  fnn0ind  12691  uz3m2nn  12914  xrltletr  13178  xrletr  13179  xrre2  13192  xrltmin  13204  xrlemin  13206  xleadd2a  13276  xleadd1  13277  xltadd2  13279  xmulasslem3  13308  xmulass  13309  xltmul2  13315  ixxdisj  13383  iooneg  13494  iccneg  13495  icoshft  13496  icoshftf1o  13497  icodisj  13499  snunioo  13501  fzen  13565  ssfzunsnext  13593  fzrev3  13614  2ffzeq  13673  fzoaddel2  13745  elfzodifsumelfzo  13756  ssfzoulel  13785  ssfzo12bi  13786  fzoopth  13787  fzoshftral  13812  adddivflid  13847  flltdivnn0lt  13862  ltdifltdiv  13863  fldiv4p1lem1div2  13864  modcyc  13935  modcyc2  13936  modaddabs  13940  muladdmod  13944  modsubmodmod  13962  modaddmodup  13966  modaddmulmod  13970  moddi  13971  modsubdir  13972  expdiv  14145  digit2  14268  nfile  14391  hashdifpr  14448  hashgt23el  14457  hashreshashfun  14472  hashf1dmcdm  14477  hash3tpexb  14527  fi1uzind  14540  ccatval1  14610  ccatass  14622  swrdval  14677  swrdnd  14688  swrd0  14692  swrdfv2  14695  pfxsuff1eqwrdeq  14732  swrdswrdlem  14737  pfxccatin12lem2a  14760  pfxccatin12lem1  14761  repswccat  14819  cshwidxmod  14836  cshwidxmodr  14837  cshf1  14843  repswcshw  14845  2cshw  14846  2cshwcom  14849  2cshwcshw  14858  cshwcsh2id  14861  ccatco  14868  2swrd2eqwrdeq  14986  wwlktovf  14989  brcnvtrclfv  15036  shftval2  15108  mulre  15168  absdiv  15342  absdiflt  15365  absdifle  15366  abs3dif  15379  cau3  15403  ello12r  15564  elo12r  15575  modfsummods  15841  geoisum1c  15930  rpnnen2lem4  16269  rpnnen2lem7  16272  addmulmodb  16319  dvdsmulc  16337  dvdsmulcr  16339  dvdsmultr1  16350  dvdsmultr2  16352  dvdssub2  16355  oexpneg  16399  divalgb  16458  ndvdsadd  16464  sadass  16525  modgcd  16586  dvdsgcd  16598  dvdsgcdb  16599  gcdass  16601  mulgcd  16602  absmulgcd  16603  rpmulgcd  16611  expgcd  16617  zexpgcd  16619  nn0seqcvgd  16624  algcvga  16633  lcmdvdsb  16667  lcmass  16668  lcmfunsnlem1  16691  lcmfunsnlem2lem1  16692  lcmfunsnlem2lem2  16693  coprmdvds  16707  coprmdvds2  16708  rpmul  16713  cncongr1  16721  cncongr2  16722  qnumdenbi  16799  modprm0  16861  coprimeprodsq  16864  pythagtriplem4  16875  pythagtriplem8  16879  pythagtriplem9  16880  pythagtriplem12  16882  pythagtriplem14  16884  pythagtriplem16  16886  pcpremul  16899  pcgcd  16934  vdwapval  17029  vdwapun  17030  prmgaplem3  17109  prmgaplem4  17110  prmgaplem7  17113  prmgapprmolem  17117  mreiincl  17644  mreincl  17647  mremre  17652  mrcss  17668  catcisolem  18163  pleval2  18387  pospo  18395  latlem  18489  latjcom  18499  latmcom  18515  lubss  18565  lubun  18567  clatglbss  18571  ipole  18586  ipolt  18587  pslem  18624  dirtr  18654  gsumsgrpccat  18895  gsumws2  18897  frmdmnd  18914  symggrplem  18939  isgrpi  19022  grpsubrcan  19083  grpinvsub  19084  grpsubeq0  19088  grpsubadd0sub  19089  grpnpcan  19094  qussub  19258  ghmsub  19290  symgpssefmnd  19462  symggrp  19466  symgextsymg  19490  gsmsymgreqlem2  19497  symgfixfolem1  19504  pmtrprfv3  19520  symggen  19536  lsmass  19735  efgsrel  19800  cntzcmn  19906  dvrcl  20482  unitdvcl  20483  dvrcan1  20487  subrngmre  20643  subrgmre  20678  rhmsubclem2  20767  rrgeq0  20781  abvsubtri  20904  abvtrivd  20909  lmodvsubval2  21012  rmodislmodlem  21024  rmodislmod  21025  lss0cl  21042  lssintcl  21059  lssincl  21060  reslmhm2  21148  lspvadd  21191  lspsntrim  21193  islbs3  21253  unichnlidl  21336  rnglidlmmgm  21349  cncrng  21508  xrsmcmn  21510  cndrng  21516  cnsrng  21521  absabv  21539  xrs1mnd  21555  psgnco  21698  zrhpsgninv  21700  zrhpsgnevpm  21706  zrhpsgnodpm  21707  zrhpsgnelbas  21709  zrhcopsgnelbas  21710  uvcresum  21908  lindfmm  21942  lindsmm  21943  evlsval2  22203  mamudm  22517  mamufacex  22518  matsubgcell  22556  matsc  22572  scmatscmide  22629  scmatrhmcl  22650  1marepvsma1  22705  m1detdiag  22719  mdetralt  22730  m2detleiblem7  22749  gsummatr01lem3  22779  gsummatr01  22781  smadiadetlem0  22783  decpmate  22888  decpmatcl  22889  pm2mpcl  22919  pm2mpghmlem2  22934  chfacfscmul0  22980  chfacfscmulgsum  22982  chfacfpmmul0  22984  chfacfpmmulgsum  22986  unopn  23025  clsss  23176  cldmre  23200  toponmre  23215  opnssneib  23237  restabs  23287  restcls  23303  restntr  23304  hausnei2  23475  cmpsublem  23521  bwth  23532  hausmapdom  23622  ptpjcn  23733  upxp  23745  ptrescn  23761  xkopjcn  23778  fbssfi  23959  snfil  23986  ufprim  24031  rnelfm  24075  flimrest  24105  fclsrest  24146  tmdgsum  24217  blpnfctr  24558  mscl  24583  xmscl  24584  xmsge0  24585  xmseq0  24586  restmetu  24692  ngpds  24726  tngngp3  24778  unitnmn0  24790  xrsxmet  24932  metds0  24973  mpomulcn  24991  cncfmptc  25036  isclmp  25221  cnlmod  25264  ncvsi  25275  cphsqrtcl  25308  cfil3i  25393  cfilres  25420  cmssmscld  25474  cmmbl  25658  voliunlem2  25675  itg2ub  25857  itgrecl  25922  r1pid  26283  eflogeq  26729  cxpadd  26806  cxpcom  26866  logbchbase  26898  relogbreexp  26902  relogbzexp  26903  relogbmulexp  26905  logbleb  26910  logblt  26911  lawcos  26943  pythag  26944  asinsinb  27024  acoscosb  27025  atantanb  27051  amgmlem  27116  lgsneg  27447  lgsne0  27461  lgsmodeq  27468  lgsmulsqcoprm  27469  gausslemma2dlem1a  27491  2sqreulem2  27578  ltsres  27788  noetainflem1  27863  ltlestr  27886  lestr  27888  nocvxmin  27910  madebdaylemold  28053  lrrecpo  28096  ltadds2im  28141  leadds1im  28142  leadds2im  28143  leadds1  28144  leadds2  28145  ltadds1  28147  addscan2  28148  addscan1  28149  subadds  28225  ltsubs1  28231  divscl  28378  oncutlt  28419  zsoring  28564  expscllem  28585  brbtwn2  29192  colinearalg  29197  eleesubd  29199  axcgrrflx  29201  axcgrtr  29202  axsegcon  29214  ax5seglem1  29215  ax5seglem2  29216  ax5seglem4  29219  axbtwnid  29226  axlowdimlem14  29242  axlowdim  29248  axcontlem5  29255  axcontlem7  29257  nb3grprlem2  29668  cplgr3v  29722  cusgrsizeindslem  29738  sizusglecusglem2  29749  umgr2v2e  29812  cusgrrusgr  29868  iswlk  29897  edginwlk  29921  uspgr2wlkeq  29932  uspgr2wlkeq2  29933  uspgr2wlkeqi  29934  wlkonprop  29943  wlkon2n0  29951  pthdadjvtx  30014  upgr2pthnlp  30018  spthonepeq  30038  pthdlem2lem  30053  crctcshwlkn0lem3  30098  crctcshwlkn0lem5  30100  wlkiswwlks2lem4  30158  wlkiswwlks2lem6  30160  wlklnwwlkln2lem  30168  wwlksnred  30178  wwlksnextbi  30180  wwlksnextwrd  30183  2pthdlem1  30216  2wlkdlem10  30221  umgr2adedgwlkonALT  30233  elwwlks2s3  30237  elwwlks2ons3im  30240  s3wwlks2on  30242  sps3wwlks2on  30243  2wspdisj  30251  2wspiundisj  30252  clwwlkgt0  30274  clwlkclwwlklem2a4  30285  clwlkclwwlklem2a  30286  clwlkclwwlk  30290  clwlkclwwlk2  30291  clwlkclwwlkfo  30297  clwwisshclwwslemlem  30301  erclwwlktr  30310  clwwlkf  30335  wwlksubclwwlk  30346  erclwwlkntr  30359  clwwlknon  30378  frcond1  30554  frgr3v  30563  3vfriswmgr  30566  frgrwopreglem4a  30598  frrusgrord0lem  30627  clwwnonrepclwwnon  30633  extwwlkfab  30640  numclwwlk1lem2f1  30645  numclwwlk1lem2fo  30646  clwlknon2num  30656  numclwwlk2lem1  30664  numclwlk2lem2f  30665  numclwlk2lem2f1o  30667  numclwwlk2  30669  frgrreggt1  30681  friendshipgt3  30686  imsmetlem  30979  nmoxr  31055  nmoolb  31060  blometi  31092  phpar2  31112  phpar  31113  ipasslem5  31124  hvadd32  31323  hvaddsub12  31327  hvaddsubass  31330  hvsubass  31333  hvsub32  31334  hvsubdistr1  31338  hvsubdistr2  31339  hvmulcan  31361  hvmulcan2  31362  hvsubcan  31363  his5  31375  his2sub  31381  hhssabloilem  31550  hhssnv  31553  shlej2  31650  pjoi0  32006  hodcl  32036  hoadd32  32072  hosubdi  32097  hosubsub2  32101  hoaddsubass  32104  hosubsub4  32107  nmoplb  32196  unop  32204  hmop  32211  nmfnlb  32213  lnopmul  32256  kbass1  32405  kbass2  32406  leopmul2i  32424  leoptr  32426  cvntr  32581  mdslmd4i  32622  mdexchi  32624  atcv1  32669  sumdmdii  32704  fcoinvbr  32887  fpwrelmapffs  33016  xreceu  33178  isinftm  33438  inlidl  33669  unitdivcld  34232  esummulc1  34412  hasheuni  34416  unelsiga  34465  inelpisys  34485  carsgsigalem  34646  signswmnd  34885  bnj545  35224  bnj594  35241  bnj1311  35353  fissorduni  35419  r1filimi  35435  fineqvac  35448  fineqvnttrclselem3  35455  fineqvinfep  35457  usgrgt2cycl  35517  subgrwlk  35519  acycgr1v  35536  cvmsf1o  35659  cvmscld  35660  satefvfmla1  35812  elnanelprv  35816  lediv2aALT  36064  gcd32  36136  fununiq  36156  dfrdg4  36338  brcolinear  36446  colinearex  36447  nn0prpwlem  36718  clsun  36724  fnemeet1  36762  fnemeet2  36763  fnejoin1  36764  fnejoin2  36765  eltail  36770  rdgeqoa  37899  nlpineqsn  37937  curf  38132  lindsadd  38147  poimirlem28  38182  cnambfre  38202  ftc1anclem4  38230  cocanfo  38253  f1ocan1fv  38260  metf1o  38289  ismtybnd  38341  ghomco  38425  isdrngo2  38492  inidl  38564  igenmin  38598  brxrn  38917  brredunds  39244  cmtvalN  39870  cvrval  39928  pmapmeet  40432  paddval  40457  paddssat  40473  elpcliN  40552  pclssN  40553  pclunN  40557  paddunN  40586  poldmj1N  40587  tendoplcl2  41437  tendoplcl  41440  dihmeet  42002  lcmineqlem1  42681  reltsub1  43030  reltsubadd2  43031  resubsub4  43033  reppncan  43037  resubdi  43040  readdcan2  43057  subresre  43075  mapco2g  43330  mzpcompact2lem  43367  eqrabdioph  43393  lerabdioph  43417  eluzrabdioph  43418  ltrabdioph  43420  nerabdioph  43421  dvdsrabdioph  43422  reglogcl  43502  rmxyadd  43533  rmyabs  43570  congadd  43578  congabseq  43586  rmydioph  43626  mendring  43800  mendlmod  43801  iocinico  43824  omge1  43909  relexp0a  44327  relexpaddss  44329  brcoffn  44641  ismnushort  44896  dvconstbi  44929  uzwo4  45658  ssin0  45660  ssinc  45690  ssdec  45691  fvmpt2bd  45773  disjf1o  45794  ssnnf1octb  45797  sub31  45894  fperiodmullem  45907  ssfiunibd  45913  infxr  45967  fmul01  46181  islptre  46220  lptre2pt  46239  limcleqr  46243  limclner  46250  limsuppnflem  46309  limsupvaluz2  46337  supcnvlimsup  46339  xlimmnfvlem2  46432  xlimmnfv  46433  xlimpnfvlem2  46436  xlimpnfv  46437  climxlim2lem  46444  coskpi2  46465  cosknegpi  46468  dvnmptdivc  46537  dvdsn1add  46538  dvnmptconst  46540  dvmptfprod  46544  dvnprodlem1  46545  dvnprodlem2  46546  ovolsplit  46587  stoweidlem60  46659  stowei  46663  dirkeritg  46701  fourierdlem70  46775  fourierdlem71  46776  fourierdlem103  46808  fourierdlem104  46809  fouriersw  46830  rrxtopnfi  46886  saluncl  46916  salexct  46933  sge0ltfirp  46999  sge0iunmpt  47017  meadjiunlem  47064  meaiuninc3v  47083  carageniuncllem1  47120  caratheodorylem1  47125  ovncvrrp  47163  ovnsubaddlem1  47169  hspmbllem2  47226  ovolval5lem3  47253  smfpimbor1lem1  47397  smfsuplem1  47410  smflimsuplem4  47422  sigarls  47456  cnambpcma  47913  elfzelfzlble  47940  submodaddmod  47966  difltmodne  47967  m1mod0mod1  47979  modmkpkne  47986  mod2addne  47989  modm2nep1  47991  modm1nep2  47993  modm1nem2  47994  fsumsplitsndif  48000  fundcmpsurinjALT  48043  iccpartiltu  48053  prproropf1olem2  48135  fmtno4prmfac  48206  2pwp1prmfmtno  48224  lighneallem4b  48243  nprmdvdsfacm1lem4  48257  mogoldbblem  48367  gbegt5  48408  sbgoldbm  48431  nnsum3primesle9  48441  nnsum4primesodd  48443  nnsum4primesoddALTV  48444  evengpoap3  48446  nnsum4primesevenALTV  48448  clnbgredg  48487  opstrgric  48573  clnbgrgrimlem  48580  grtrif1o  48589  isubgr3stgrlem1  48613  isubgr3stgrlem4  48616  gpgusgralem  48703  gpg3nbgrvtx0  48723  isupwlk  48783  lidldomnnring  48883  2zrngacmnd  48895  rhmsubcALTVlem2  48929  fprmappr  49003  zlmodzxzscm  49015  gsumlsscl  49038  lincvalsng  49074  lincvalpr  49076  lincdifsn  49082  linc1  49083  lincellss  49084  fdivmpt  49198  digexp  49265  2arymaptfo  49312  line  49390  rrxline  49392  itsclc0xyqsolr  49427  iscnrm3r  49604  resipos  49631  amgmwlem  50458