Theorem 3adant1 1142

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  3ad2ant2  1146  3ad2ant3  1147  3simpc  1162  eupickb  2661  spc3egv  3561  reuhyp  5374  predtrss  6304  onunel  6448  funopg  6550  funprg  6570  funtpg  6571  funcnvtp  6579  unima  6937  fvun1  6953  fnreseql  7024  xpprsng  7117  ftpg  7134  f1ounsn  7251  f13dfv  7253  f1ocoima  7282  f1ofvswap  7285  mpoeq3ia  7469  ordunel  7802  fex2  7912  funexw  7928  poxp  8102  poxp2  8117  poxp3  8124  poseq  8132  suppval1  8140  wfr3g  8294  smores3  8318  oaord  8510  oacan  8511  oaword  8512  omord  8531  omcan  8532  omwordri  8535  odi  8542  omass  8543  oeord  8552  oecan  8553  oewordri  8556  oeordsuc  8558  nnaord  8583  nnaordr  8584  nndi  8587  nnmass  8588  nnaword  8591  nnmord  8596  nnmwordri  8600  naddelim  8651  naddel1  8652  naddel2  8653  naddss1  8654  naddss2  8655  naddasslem2  8660  nadd32  8662  erov  8790  ecopovtrn  8796  ixpf  8896  f1oen4g  8939  f1dom4g  8940  mapxpen  9109  ssfi  9135  sbthfilem  9160  sbthfi  9161  onomeneq  9176  fimax2g  9224  unbnn  9234  funisfsupp  9307  inelfi  9358  elfiun  9370  sup0  9407  suppr  9412  infpr  9445  ttrclss  9669  frr3g  9708  r111  9727  dif1card  9960  ackbij1lem16  10184  cff1  10209  cfflb  10210  cfsmolem  10221  fin23lem34  10297  hsmexlem2  10378  axcc3  10389  domtriomlem  10393  axdc3lem4  10404  axdc4lem  10406  axcclem  10408  konigthlem  10520  gchdomtri  10581  tskpr  10722  tskop  10723  tskuni  10735  tskun  10738  gruop  10757  gruun  10758  grudomon  10769  adderpqlem  10906  mulerpqlem  10907  addassnq  10910  mulassnq  10911  distrnq  10913  ltsonq  10921  ltanq  10923  ltmnq  10924  genpass  10961  distrlem1pr  10977  distrlem4pr  10978  ltsopr  10984  adddir  11164  axlttrn  11249  ltletr  11269  letr  11271  mul32  11343  mul31  11344  add32  11396  subsub23  11429  addsubass  11434  subcan2  11450  subsub2  11453  nppcan2  11456  sub32  11459  nnncan  11460  nnncan2  11462  pnpcan2  11465  subdi  11614  subdir  11615  receu  11826  mulcan1g  11834  mulcan2g  11835  divmul3  11844  divrec  11855  divrec2  11856  div11  11867  divsubdir  11878  subdivcomb2  11881  divdiv1  11896  redivcl  11904  div2neg  11908  ltmul2  12036  lemul1  12037  lemul2  12038  lemul2a  12040  lediv1  12051  gt0div  12052  ge0div  12053  mulsuble0b  12058  ltdivmul  12061  ledivmul  12062  ltdivmul2  12063  ledivmul2  12065  lemuldiv  12066  ltdiv23  12077  lediv23  12078  ledivp1i  12111  ltdivp1i  12112  uzind2  12660  nn0ind  12662  fnn0ind  12666  uz3m2nn  12889  xrltletr  13153  xrletr  13154  xrre2  13167  xrltmin  13179  xrlemin  13181  xleadd2a  13251  xleadd1  13252  xltadd2  13254  xmulasslem3  13283  xmulass  13284  xltmul2  13290  ixxdisj  13358  iooneg  13469  iccneg  13470  icoshft  13471  icoshftf1o  13472  icodisj  13474  snunioo  13476  fzen  13540  ssfzunsnext  13568  fzrev3  13589  2ffzeq  13648  fzoaddel2  13720  elfzodifsumelfzo  13731  ssfzoulel  13760  ssfzo12bi  13761  fzoopth  13762  fzoshftral  13787  adddivflid  13822  flltdivnn0lt  13837  ltdifltdiv  13838  fldiv4p1lem1div2  13839  modcyc  13910  modcyc2  13911  modaddabs  13915  muladdmod  13919  modsubmodmod  13937  modaddmodup  13941  modaddmulmod  13945  moddi  13946  modsubdir  13947  expdiv  14120  digit2  14243  nfile  14366  hashdifpr  14422  hashgt23el  14431  hashreshashfun  14446  hashf1dmcdm  14451  hash3tpexb  14501  fi1uzind  14514  ccatval1  14584  ccatass  14596  swrdval  14651  swrdnd  14662  swrd0  14666  swrdfv2  14669  pfxsuff1eqwrdeq  14706  swrdswrdlem  14711  pfxccatin12lem2a  14734  pfxccatin12lem1  14735  repswccat  14793  cshwidxmod  14810  cshwidxmodr  14811  cshf1  14817  repswcshw  14819  2cshw  14820  2cshwcom  14823  2cshwcshw  14832  cshwcsh2id  14835  ccatco  14842  2swrd2eqwrdeq  14960  wwlktovf  14963  brcnvtrclfv  15010  shftval2  15082  mulre  15139  absdiv  15313  absdiflt  15336  absdifle  15337  abs3dif  15350  cau3  15374  ello12r  15535  elo12r  15546  modfsummods  15812  geoisum1c  15901  rpnnen2lem4  16240  rpnnen2lem7  16243  addmulmodb  16290  dvdsmulc  16308  dvdsmulcr  16310  dvdsmultr1  16321  dvdsmultr2  16323  dvdssub2  16326  oexpneg  16370  divalgb  16429  ndvdsadd  16435  sadass  16496  modgcd  16557  dvdsgcd  16569  dvdsgcdb  16570  gcdass  16572  mulgcd  16573  absmulgcd  16574  rpmulgcd  16582  expgcd  16588  zexpgcd  16590  nn0seqcvgd  16595  algcvga  16604  lcmdvdsb  16638  lcmass  16639  lcmfunsnlem1  16662  lcmfunsnlem2lem1  16663  lcmfunsnlem2lem2  16664  coprmdvds  16678  coprmdvds2  16679  rpmul  16684  cncongr1  16692  cncongr2  16693  qnumdenbi  16770  modprm0  16832  coprimeprodsq  16835  pythagtriplem4  16846  pythagtriplem8  16850  pythagtriplem9  16851  pythagtriplem12  16853  pythagtriplem14  16855  pythagtriplem16  16857  pcpremul  16870  pcgcd  16905  vdwapval  17000  vdwapun  17001  prmgaplem3  17080  prmgaplem4  17081  prmgaplem7  17084  prmgapprmolem  17088  mreiincl  17615  mreincl  17618  mremre  17623  mrcss  17639  catcisolem  18134  pleval2  18358  pospo  18366  latlem  18460  latjcom  18470  latmcom  18486  lubss  18536  lubun  18538  clatglbss  18542  ipole  18557  ipolt  18558  pslem  18595  dirtr  18625  gsumsgrpccat  18865  gsumws2  18867  frmdmnd  18884  symggrplem  18909  isgrpi  18992  grpsubrcan  19054  grpinvsub  19055  grpsubeq0  19059  grpsubadd0sub  19060  grpnpcan  19065  qussub  19223  ghmsub  19255  symgpssefmnd  19427  symggrp  19431  symgextsymg  19455  gsmsymgreqlem2  19462  symgfixfolem1  19469  pmtrprfv3  19485  symggen  19501  lsmass  19700  efgsrel  19765  cntzcmn  19871  dvrcl  20440  unitdvcl  20441  dvrcan1  20445  subrngmre  20599  subrgmre  20634  rhmsubclem2  20723  rrgeq0  20737  abvsubtri  20864  abvtrivd  20869  lmodvsubval2  20972  rmodislmodlem  20984  rmodislmod  20985  lss0cl  21002  lssintcl  21019  lssincl  21020  reslmhm2  21108  lspvadd  21151  lspsntrim  21153  islbs3  21213  rnglidlmmgm  21303  cncrng  21433  xrsmcmn  21435  cndrng  21441  cnsrng  21446  absabv  21464  xrs1mnd  21480  psgnco  21623  zrhpsgninv  21625  zrhpsgnevpm  21631  zrhpsgnodpm  21632  zrhpsgnelbas  21634  zrhcopsgnelbas  21635  uvcresum  21833  lindfmm  21867  lindsmm  21868  evlsval2  22128  mamudm  22443  mamufacex  22444  matsubgcell  22482  matsc  22498  scmatscmide  22555  scmatrhmcl  22576  1marepvsma1  22631  m1detdiag  22645  mdetralt  22656  m2detleiblem7  22675  gsummatr01lem3  22705  gsummatr01  22707  smadiadetlem0  22709  decpmate  22814  decpmatcl  22815  pm2mpcl  22845  pm2mpghmlem2  22860  chfacfscmul0  22906  chfacfscmulgsum  22908  chfacfpmmul0  22910  chfacfpmmulgsum  22912  unopn  22951  clsss  23102  cldmre  23126  toponmre  23141  opnssneib  23163  restabs  23213  restcls  23229  restntr  23230  hausnei2  23401  cmpsublem  23447  bwth  23458  hausmapdom  23548  ptpjcn  23659  upxp  23671  ptrescn  23687  xkopjcn  23704  fbssfi  23885  snfil  23912  ufprim  23957  rnelfm  24001  flimrest  24031  fclsrest  24072  tmdgsum  24143  blpnfctr  24484  mscl  24509  xmscl  24510  xmsge0  24511  xmseq0  24512  restmetu  24618  ngpds  24652  tngngp3  24704  unitnmn0  24716  xrsxmet  24858  metds0  24899  mpomulcn  24917  cncfmptc  24962  isclmp  25147  cnlmod  25190  ncvsi  25201  cphsqrtcl  25234  cfil3i  25319  cfilres  25346  cmssmscld  25400  cmmbl  25584  voliunlem2  25601  itg2ub  25783  itgrecl  25848  r1pid  26209  eflogeq  26655  cxpadd  26732  cxpcom  26792  logbchbase  26824  relogbreexp  26828  relogbzexp  26829  relogbmulexp  26831  logbleb  26836  logblt  26837  lawcos  26869  pythag  26870  asinsinb  26950  acoscosb  26951  atantanb  26977  amgmlem  27042  lgsneg  27373  lgsne0  27387  lgsmodeq  27394  lgsmulsqcoprm  27395  gausslemma2dlem1a  27417  2sqreulem2  27504  ltsres  27714  noetainflem1  27789  ltlestr  27812  lestr  27814  nocvxmin  27836  madebdaylemold  27979  lrrecpo  28022  ltadds2im  28067  leadds1im  28068  leadds2im  28069  leadds1  28070  leadds2  28071  ltadds1  28073  addscan2  28074  addscan1  28075  subadds  28151  ltsubs1  28157  divscl  28304  oncutlt  28345  zsoring  28490  expscllem  28511  brbtwn2  29063  colinearalg  29068  eleesubd  29070  axcgrrflx  29072  axcgrtr  29073  axsegcon  29085  ax5seglem1  29086  ax5seglem2  29087  ax5seglem4  29090  axbtwnid  29097  axlowdimlem14  29113  axlowdim  29119  axcontlem5  29126  axcontlem7  29128  nb3grprlem2  29539  cplgr3v  29593  cusgrsizeindslem  29609  sizusglecusglem2  29620  umgr2v2e  29683  cusgrrusgr  29739  iswlk  29768  edginwlk  29792  uspgr2wlkeq  29803  uspgr2wlkeq2  29804  uspgr2wlkeqi  29805  wlkonprop  29814  wlkon2n0  29822  pthdadjvtx  29885  upgr2pthnlp  29889  spthonepeq  29909  pthdlem2lem  29924  crctcshwlkn0lem3  29969  crctcshwlkn0lem5  29971  wlkiswwlks2lem4  30029  wlkiswwlks2lem6  30031  wlklnwwlkln2lem  30039  wwlksnred  30049  wwlksnextbi  30051  wwlksnextwrd  30054  2pthdlem1  30087  2wlkdlem10  30092  umgr2adedgwlkonALT  30104  elwwlks2s3  30108  elwwlks2ons3im  30111  s3wwlks2on  30113  sps3wwlks2on  30114  2wspdisj  30122  2wspiundisj  30123  clwwlkgt0  30145  clwlkclwwlklem2a4  30156  clwlkclwwlklem2a  30157  clwlkclwwlk  30161  clwlkclwwlk2  30162  clwlkclwwlkfo  30168  clwwisshclwwslemlem  30172  erclwwlktr  30181  clwwlkf  30206  wwlksubclwwlk  30217  erclwwlkntr  30230  clwwlknon  30249  frcond1  30425  frgr3v  30434  3vfriswmgr  30437  frgrwopreglem4a  30469  frrusgrord0lem  30498  clwwnonrepclwwnon  30504  extwwlkfab  30511  numclwwlk1lem2f1  30516  numclwwlk1lem2fo  30517  clwlknon2num  30527  numclwwlk2lem1  30535  numclwlk2lem2f  30536  numclwlk2lem2f1o  30538  numclwwlk2  30540  frgrreggt1  30552  friendshipgt3  30557  imsmetlem  30850  nmoxr  30926  nmoolb  30931  blometi  30963  phpar2  30983  phpar  30984  ipasslem5  30995  hvadd32  31194  hvaddsub12  31198  hvaddsubass  31201  hvsubass  31204  hvsub32  31205  hvsubdistr1  31209  hvsubdistr2  31210  hvmulcan  31232  hvmulcan2  31233  hvsubcan  31234  his5  31246  his2sub  31252  hhssabloilem  31421  hhssnv  31424  shlej2  31521  pjoi0  31877  hodcl  31907  hoadd32  31943  hosubdi  31968  hosubsub2  31972  hoaddsubass  31975  hosubsub4  31978  nmoplb  32067  unop  32075  hmop  32082  nmfnlb  32084  lnopmul  32127  kbass1  32276  kbass2  32277  leopmul2i  32295  leoptr  32297  cvntr  32452  mdslmd4i  32493  mdexchi  32495  atcv1  32540  sumdmdii  32575  fcoinvbr  32765  fpwrelmapffs  32897  xreceu  33060  isinftm  33322  unitdivcld  34159  esummulc1  34339  hasheuni  34343  unelsiga  34392  inelpisys  34412  carsgsigalem  34573  signswmnd  34812  bnj545  35151  bnj594  35168  bnj1311  35280  fissorduni  35346  r1filimi  35360  fineqvac  35373  fineqvnttrclselem3  35380  fineqvinfep  35382  usgrgt2cycl  35441  subgrwlk  35443  acycgr1v  35460  cvmsf1o  35583  cvmscld  35584  satefvfmla1  35736  elnanelprv  35740  lediv2aALT  35988  gcd32  36060  fununiq  36080  dfrdg4  36262  brcolinear  36370  colinearex  36371  nn0prpwlem  36643  clsun  36649  fnemeet1  36687  fnemeet2  36688  fnejoin1  36689  fnejoin2  36690  eltail  36695  rdgeqoa  37825  nlpineqsn  37863  curf  38058  lindsadd  38073  poimirlem28  38108  cnambfre  38128  ftc1anclem4  38156  cocanfo  38179  f1ocan1fv  38186  metf1o  38215  ismtybnd  38267  ghomco  38351  isdrngo2  38418  inidl  38490  igenmin  38524  brxrn  38843  brredunds  39170  cmtvalN  39796  cvrval  39854  pmapmeet  40358  paddval  40383  paddssat  40399  elpcliN  40478  pclssN  40479  pclunN  40483  paddunN  40512  poldmj1N  40513  tendoplcl2  41363  tendoplcl  41366  dihmeet  41928  lcmineqlem1  42607  reltsub1  42956  reltsubadd2  42957  resubsub4  42959  reppncan  42963  resubdi  42966  readdcan2  42983  subresre  43001  mapco2g  43256  mzpcompact2lem  43293  eqrabdioph  43319  lerabdioph  43343  eluzrabdioph  43344  ltrabdioph  43346  nerabdioph  43347  dvdsrabdioph  43348  reglogcl  43428  rmxyadd  43459  rmyabs  43496  congadd  43504  congabseq  43512  rmydioph  43552  mendring  43726  mendlmod  43727  iocinico  43750  omge1  43835  relexp0a  44253  relexpaddss  44255  brcoffn  44567  ismnushort  44838  dvconstbi  44871  uzwo4  45594  ssin0  45596  ssinc  45626  ssdec  45627  fvmpt2bd  45709  disjf1o  45730  ssnnf1octb  45733  sub31  45830  fperiodmullem  45843  ssfiunibd  45849  infxr  45903  fmul01  46117  islptre  46156  lptre2pt  46175  limcleqr  46179  limclner  46186  limsuppnflem  46245  limsupvaluz2  46273  supcnvlimsup  46275  xlimmnfvlem2  46368  xlimmnfv  46369  xlimpnfvlem2  46372  xlimpnfv  46373  climxlim2lem  46380  coskpi2  46401  cosknegpi  46404  dvnmptdivc  46473  dvdsn1add  46474  dvnmptconst  46476  dvmptfprod  46480  dvnprodlem1  46481  dvnprodlem2  46482  ovolsplit  46523  stoweidlem60  46595  stowei  46599  dirkeritg  46637  fourierdlem70  46711  fourierdlem71  46712  fourierdlem103  46744  fourierdlem104  46745  fouriersw  46766  rrxtopnfi  46822  saluncl  46852  salexct  46869  sge0ltfirp  46935  sge0iunmpt  46953  meadjiunlem  47000  meaiuninc3v  47019  carageniuncllem1  47056  caratheodorylem1  47061  ovncvrrp  47099  ovnsubaddlem1  47105  hspmbllem2  47162  ovolval5lem3  47189  smfpimbor1lem1  47333  smfsuplem1  47346  smflimsuplem4  47358  sigarls  47392  cnambpcma  47849  elfzelfzlble  47876  submodaddmod  47902  difltmodne  47903  m1mod0mod1  47915  modmkpkne  47922  mod2addne  47925  modm2nep1  47927  modm1nep2  47929  modm1nem2  47930  fsumsplitsndif  47936  fundcmpsurinjALT  47979  iccpartiltu  47989  prproropf1olem2  48071  fmtno4prmfac  48142  2pwp1prmfmtno  48160  lighneallem4b  48179  nprmdvdsfacm1lem4  48193  mogoldbblem  48303  gbegt5  48344  sbgoldbm  48367  nnsum3primesle9  48377  nnsum4primesodd  48379  nnsum4primesoddALTV  48380  evengpoap3  48382  nnsum4primesevenALTV  48384  clnbgredg  48423  opstrgric  48509  clnbgrgrimlem  48516  grtrif1o  48525  isubgr3stgrlem1  48549  isubgr3stgrlem4  48552  gpgusgralem  48639  gpg3nbgrvtx0  48659  isupwlk  48719  lidldomnnring  48819  2zrngacmnd  48831  rhmsubcALTVlem2  48865  fprmappr  48928  zlmodzxzscm  48940  gsumlsscl  48963  lincvalsng  48999  lincvalpr  49001  lincdifsn  49007  linc1  49008  lincellss  49009  fdivmpt  49123  digexp  49190  2arymaptfo  49237  line  49315  rrxline  49317  itsclc0xyqsolr  49352  iscnrm3r  49530  resipos  49557  amgmwlem  50384