Theorem 3adant1 1136

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  3ad2ant2  1140  3ad2ant3  1141  3simpc  1156  eupickb  2639  spc3egv  3541  reuhyp  5349  predtrss  6273  onunel  6417  funopg  6519  funprg  6539  funtpg  6540  funcnvtp  6548  unima  6902  fvun1  6918  fnreseql  6989  xpprsng  7082  ftpg  7099  f1ounsn  7216  f13dfv  7218  f1ocoima  7247  f1ofvswap  7250  mpoeq3ia  7434  ordunel  7767  fex2  7876  funexw  7894  poxp  8068  poxp2  8083  poxp3  8090  poseq  8098  suppval1  8106  wfr3g  8259  smores3  8283  oaord  8472  oacan  8473  oaword  8474  omord  8493  omcan  8494  omwordri  8497  odi  8504  omass  8505  oeord  8514  oecan  8515  oewordri  8518  oeordsuc  8520  nnaord  8545  nnaordr  8546  nndi  8549  nnmass  8550  nnaword  8553  nnmord  8558  nnmwordri  8562  naddelim  8612  naddel1  8613  naddel2  8614  naddss1  8615  naddss2  8616  naddasslem2  8621  nadd32  8623  erov  8751  ecopovtrn  8757  ixpf  8858  f1oen4g  8901  f1dom4g  8902  mapxpen  9071  ssfi  9097  sbthfilem  9122  sbthfi  9123  onomeneq  9138  fimax2g  9186  unbnn  9196  funisfsupp  9270  inelfi  9321  elfiun  9333  sup0  9370  suppr  9375  infpr  9408  ttrclss  9632  frr3g  9671  r111  9690  dif1card  9923  ackbij1lem16  10147  cff1  10171  cfflb  10172  cfsmolem  10183  fin23lem34  10259  hsmexlem2  10340  axcc3  10351  domtriomlem  10355  axdc3lem4  10366  axdc4lem  10368  axcclem  10370  konigthlem  10482  gchdomtri  10543  tskpr  10684  tskop  10685  tskuni  10697  tskun  10700  gruop  10719  gruun  10720  grudomon  10731  adderpqlem  10868  mulerpqlem  10869  addassnq  10872  mulassnq  10873  distrnq  10875  ltsonq  10883  ltanq  10885  ltmnq  10886  genpass  10923  distrlem1pr  10939  distrlem4pr  10940  ltsopr  10946  adddir  11126  axlttrn  11209  ltletr  11229  letr  11231  mul32  11303  mul31  11304  add32  11356  subsub23  11389  addsubass  11394  subcan2  11410  subsub2  11413  nppcan2  11416  sub32  11419  nnncan  11420  nnncan2  11422  pnpcan2  11425  subdi  11574  subdir  11575  receu  11786  mulcan1g  11794  mulcan2g  11795  divmul3  11805  divrec  11816  divrec2  11817  div11  11828  divsubdir  11839  subdivcomb2  11842  divdiv1  11857  redivcl  11865  div2neg  11869  ltmul2  11997  lemul1  11998  lemul2  11999  lemul2a  12001  lediv1  12012  gt0div  12013  ge0div  12014  mulsuble0b  12019  ltdivmul  12022  ledivmul  12023  ltdivmul2  12024  ledivmul2  12026  lemuldiv  12027  ltdiv23  12038  lediv23  12039  ledivp1i  12072  ltdivp1i  12073  uzind2  12613  nn0ind  12615  fnn0ind  12619  uz3m2nn  12835  xrltletr  13099  xrletr  13100  xrre2  13113  xrltmin  13125  xrlemin  13127  xleadd2a  13197  xleadd1  13198  xltadd2  13200  xmulasslem3  13229  xmulass  13230  xltmul2  13236  ixxdisj  13304  iooneg  13415  iccneg  13416  icoshft  13417  icoshftf1o  13418  icodisj  13420  snunioo  13422  fzen  13486  ssfzunsnext  13514  fzrev3  13535  2ffzeq  13594  fzoaddel2  13666  elfzodifsumelfzo  13677  ssfzoulel  13706  ssfzo12bi  13707  fzoopth  13708  fzoshftral  13733  adddivflid  13768  flltdivnn0lt  13783  ltdifltdiv  13784  fldiv4p1lem1div2  13785  modcyc  13856  modcyc2  13857  modaddabs  13861  muladdmod  13865  modsubmodmod  13883  modaddmodup  13887  modaddmulmod  13891  moddi  13892  modsubdir  13893  expdiv  14066  digit2  14189  nfile  14312  hashdifpr  14368  hashgt23el  14377  hashreshashfun  14392  hashf1dmcdm  14397  hash3tpexb  14447  fi1uzind  14460  ccatval1  14530  ccatass  14542  swrdval  14597  swrdnd  14608  swrd0  14612  swrdfv2  14615  pfxsuff1eqwrdeq  14652  swrdswrdlem  14657  pfxccatin12lem2a  14680  pfxccatin12lem1  14681  repswccat  14739  cshwidxmod  14756  cshwidxmodr  14757  cshf1  14763  repswcshw  14765  2cshw  14766  2cshwcom  14769  2cshwcshw  14778  cshwcsh2id  14781  ccatco  14788  2swrd2eqwrdeq  14906  wwlktovf  14909  brcnvtrclfv  14956  shftval2  15028  mulre  15074  absdiv  15248  absdiflt  15271  absdifle  15272  abs3dif  15285  cau3  15309  ello12r  15470  elo12r  15481  modfsummods  15747  geoisum1c  15836  rpnnen2lem4  16175  rpnnen2lem7  16178  addmulmodb  16225  dvdsmulc  16243  dvdsmulcr  16245  dvdsmultr1  16256  dvdsmultr2  16258  dvdssub2  16261  oexpneg  16305  divalgb  16364  ndvdsadd  16370  sadass  16431  modgcd  16492  dvdsgcd  16504  dvdsgcdb  16505  gcdass  16507  mulgcd  16508  absmulgcd  16509  rpmulgcd  16517  expgcd  16523  zexpgcd  16525  nn0seqcvgd  16530  algcvga  16539  lcmdvdsb  16573  lcmass  16574  lcmfunsnlem1  16597  lcmfunsnlem2lem1  16598  lcmfunsnlem2lem2  16599  coprmdvds  16613  coprmdvds2  16614  rpmul  16619  cncongr1  16627  cncongr2  16628  qnumdenbi  16705  modprm0  16767  coprimeprodsq  16770  pythagtriplem4  16781  pythagtriplem8  16785  pythagtriplem9  16786  pythagtriplem12  16788  pythagtriplem14  16790  pythagtriplem16  16792  pcpremul  16805  pcgcd  16840  vdwapval  16935  vdwapun  16936  prmgaplem3  17015  prmgaplem4  17016  prmgaplem7  17019  prmgapprmolem  17023  mreiincl  17549  mreincl  17552  mremre  17557  mrcss  17573  catcisolem  18068  pleval2  18292  pospo  18300  latlem  18394  latjcom  18404  latmcom  18420  lubss  18470  lubun  18472  clatglbss  18476  ipole  18491  ipolt  18492  pslem  18529  dirtr  18559  gsumsgrpccat  18799  gsumws2  18801  frmdmnd  18818  symggrplem  18843  isgrpi  18926  grpsubrcan  18988  grpinvsub  18989  grpsubeq0  18993  grpsubadd0sub  18994  grpnpcan  18999  qussub  19157  ghmsub  19190  symgpssefmnd  19362  symggrp  19366  symgextsymg  19390  gsmsymgreqlem2  19397  symgfixfolem1  19404  pmtrprfv3  19420  symggen  19436  lsmass  19635  efgsrel  19700  cntzcmn  19806  dvrcl  20375  unitdvcl  20376  dvrcan1  20380  subrngmre  20534  subrgmre  20569  rhmsubclem2  20658  rrgeq0  20672  abvsubtri  20799  abvtrivd  20804  lmodvsubval2  20907  rmodislmodlem  20919  rmodislmod  20920  lss0cl  20937  lssintcl  20954  lssincl  20955  reslmhm2  21043  lspvadd  21086  lspsntrim  21088  islbs3  21148  rnglidlmmgm  21238  cncrng  21368  xrsmcmn  21370  cndrng  21376  cnsrng  21381  absabv  21399  xrs1mnd  21415  psgnco  21558  zrhpsgninv  21560  zrhpsgnevpm  21566  zrhpsgnodpm  21567  zrhpsgnelbas  21569  zrhcopsgnelbas  21570  uvcresum  21768  lindfmm  21802  lindsmm  21803  evlsval2  22063  mamudm  22378  mamufacex  22379  matsubgcell  22417  matsc  22433  scmatscmide  22490  scmatrhmcl  22511  1marepvsma1  22566  m1detdiag  22580  mdetralt  22591  m2detleiblem7  22610  gsummatr01lem3  22640  gsummatr01  22642  smadiadetlem0  22644  decpmate  22749  decpmatcl  22750  pm2mpcl  22780  pm2mpghmlem2  22795  chfacfscmul0  22841  chfacfscmulgsum  22843  chfacfpmmul0  22845  chfacfpmmulgsum  22847  unopn  22886  clsss  23037  cldmre  23061  toponmre  23076  opnssneib  23098  restabs  23148  restcls  23164  restntr  23165  hausnei2  23336  cmpsublem  23382  bwth  23393  hausmapdom  23483  ptpjcn  23594  upxp  23606  ptrescn  23622  xkopjcn  23639  fbssfi  23820  snfil  23847  ufprim  23892  rnelfm  23936  flimrest  23966  fclsrest  24007  tmdgsum  24078  blpnfctr  24419  mscl  24444  xmscl  24445  xmsge0  24446  xmseq0  24447  restmetu  24553  ngpds  24587  tngngp3  24639  unitnmn0  24651  xrsxmet  24793  metds0  24834  mpomulcn  24852  cncfmptc  24897  isclmp  25082  cnlmod  25125  ncvsi  25136  cphsqrtcl  25169  cfil3i  25254  cfilres  25281  cmssmscld  25335  cmmbl  25519  voliunlem2  25536  itg2ub  25718  itgrecl  25783  r1pid  26144  eflogeq  26584  cxpadd  26661  cxpcom  26721  logbchbase  26753  relogbreexp  26757  relogbzexp  26758  relogbmulexp  26760  logbleb  26765  logblt  26766  lawcos  26798  pythag  26799  asinsinb  26879  acoscosb  26880  atantanb  26906  amgmlem  26971  lgsneg  27302  lgsne0  27316  lgsmodeq  27323  lgsmulsqcoprm  27324  gausslemma2dlem1a  27346  2sqreulem2  27433  ltsres  27644  noetainflem1  27719  ltlestr  27742  lestr  27744  nocvxmin  27765  madebdaylemold  27908  lrrecpo  27951  ltadds2im  27996  leadds1im  27997  leadds2im  27998  leadds1  27999  leadds2  28000  ltadds1  28002  addscan2  28003  addscan1  28004  subadds  28080  ltsubs1  28086  divscl  28233  oncutlt  28274  zsoring  28419  expscllem  28440  brbtwn2  28992  colinearalg  28997  eleesubd  28999  axcgrrflx  29001  axcgrtr  29002  axsegcon  29014  ax5seglem1  29015  ax5seglem2  29016  ax5seglem4  29019  axbtwnid  29026  axlowdimlem14  29042  axlowdim  29048  axcontlem5  29055  axcontlem7  29057  nb3grprlem2  29468  cplgr3v  29522  cusgrsizeindslem  29538  sizusglecusglem2  29549  umgr2v2e  29612  cusgrrusgr  29668  iswlk  29697  edginwlk  29721  uspgr2wlkeq  29732  uspgr2wlkeq2  29733  uspgr2wlkeqi  29734  wlkonprop  29743  wlkon2n0  29751  pthdadjvtx  29814  upgr2pthnlp  29818  spthonepeq  29838  pthdlem2lem  29853  crctcshwlkn0lem3  29898  crctcshwlkn0lem5  29900  wlkiswwlks2lem4  29958  wlkiswwlks2lem6  29960  wlklnwwlkln2lem  29968  wwlksnred  29978  wwlksnextbi  29980  wwlksnextwrd  29983  2pthdlem1  30016  2wlkdlem10  30021  umgr2adedgwlkonALT  30033  elwwlks2s3  30037  elwwlks2ons3im  30040  s3wwlks2on  30042  sps3wwlks2on  30043  2wspdisj  30051  2wspiundisj  30052  clwwlkgt0  30074  clwlkclwwlklem2a4  30085  clwlkclwwlklem2a  30086  clwlkclwwlk  30090  clwlkclwwlk2  30091  clwlkclwwlkfo  30097  clwwisshclwwslemlem  30101  erclwwlktr  30110  clwwlkf  30135  wwlksubclwwlk  30146  erclwwlkntr  30159  clwwlknon  30178  frcond1  30354  frgr3v  30363  3vfriswmgr  30366  frgrwopreglem4a  30398  frrusgrord0lem  30427  clwwnonrepclwwnon  30433  extwwlkfab  30440  numclwwlk1lem2f1  30445  numclwwlk1lem2fo  30446  clwlknon2num  30456  numclwwlk2lem1  30464  numclwlk2lem2f  30465  numclwlk2lem2f1o  30467  numclwwlk2  30469  frgrreggt1  30481  friendshipgt3  30486  imsmetlem  30779  nmoxr  30855  nmoolb  30860  blometi  30892  phpar2  30912  phpar  30913  ipasslem5  30924  hvadd32  31123  hvaddsub12  31127  hvaddsubass  31130  hvsubass  31133  hvsub32  31134  hvsubdistr1  31138  hvsubdistr2  31139  hvmulcan  31161  hvmulcan2  31162  hvsubcan  31163  his5  31175  his2sub  31181  hhssabloilem  31350  hhssnv  31353  shlej2  31450  pjoi0  31806  hodcl  31836  hoadd32  31872  hosubdi  31897  hosubsub2  31901  hoaddsubass  31904  hosubsub4  31907  nmoplb  31996  unop  32004  hmop  32011  nmfnlb  32013  lnopmul  32056  kbass1  32205  kbass2  32206  leopmul2i  32224  leoptr  32226  cvntr  32381  mdslmd4i  32422  mdexchi  32424  atcv1  32469  sumdmdii  32504  fcoinvbr  32694  fpwrelmapffs  32826  xreceu  33000  isinftm  33262  unitdivcld  34085  esummulc1  34265  hasheuni  34269  unelsiga  34318  inelpisys  34338  carsgsigalem  34499  signswmnd  34741  bnj545  35077  bnj594  35094  bnj1311  35206  fissorduni  35271  r1filimi  35284  fineqvac  35297  fineqvnttrclselem3  35304  fineqvinfep  35306  usgrgt2cycl  35358  subgrwlk  35360  acycgr1v  35377  cvmsf1o  35500  cvmscld  35501  satefvfmla1  35653  elnanelprv  35657  lediv2aALT  35905  gcd32  35977  fununiq  35997  dfrdg4  36179  brcolinear  36287  colinearex  36288  nn0prpwlem  36550  clsun  36556  fnemeet1  36594  fnemeet2  36595  fnejoin1  36596  fnejoin2  36597  eltail  36602  rdgeqoa  37732  nlpineqsn  37770  curf  37965  lindsadd  37980  poimirlem28  38015  cnambfre  38035  ftc1anclem4  38063  cocanfo  38086  f1ocan1fv  38093  metf1o  38122  ismtybnd  38174  ghomco  38258  isdrngo2  38325  inidl  38397  igenmin  38431  brxrn  38750  brredunds  39077  cmtvalN  39703  cvrval  39761  pmapmeet  40265  paddval  40290  paddssat  40306  elpcliN  40385  pclssN  40386  pclunN  40390  paddunN  40419  poldmj1N  40420  tendoplcl2  41270  tendoplcl  41273  dihmeet  41835  lcmineqlem1  42514  reltsub1  42863  reltsubadd2  42864  resubsub4  42866  reppncan  42870  resubdi  42873  readdcan2  42890  subresre  42908  mapco2g  43163  mzpcompact2lem  43200  eqrabdioph  43226  lerabdioph  43250  eluzrabdioph  43251  ltrabdioph  43253  nerabdioph  43254  dvdsrabdioph  43255  reglogcl  43335  rmxyadd  43366  rmyabs  43403  congadd  43411  congabseq  43419  rmydioph  43459  mendring  43633  mendlmod  43634  iocinico  43657  omge1  43742  relexp0a  44160  relexpaddss  44162  brcoffn  44474  ismnushort  44745  dvconstbi  44778  uzwo4  45501  ssin0  45503  ssinc  45534  ssdec  45535  fvmpt2bd  45617  disjf1o  45638  ssnnf1octb  45641  sub31  45738  fperiodmullem  45751  ssfiunibd  45757  infxr  45811  fmul01  46025  islptre  46064  lptre2pt  46083  limcleqr  46087  limclner  46094  limsuppnflem  46153  limsupvaluz2  46181  supcnvlimsup  46183  xlimmnfvlem2  46276  xlimmnfv  46277  xlimpnfvlem2  46280  xlimpnfv  46281  climxlim2lem  46288  coskpi2  46309  cosknegpi  46312  dvnmptdivc  46381  dvdsn1add  46382  dvnmptconst  46384  dvmptfprod  46388  dvnprodlem1  46389  dvnprodlem2  46390  ovolsplit  46431  stoweidlem60  46503  stowei  46507  dirkeritg  46545  fourierdlem70  46619  fourierdlem71  46620  fourierdlem103  46652  fourierdlem104  46653  fouriersw  46674  rrxtopnfi  46730  saluncl  46760  salexct  46777  sge0ltfirp  46843  sge0iunmpt  46861  meadjiunlem  46908  meaiuninc3v  46927  carageniuncllem1  46964  caratheodorylem1  46969  ovncvrrp  47007  ovnsubaddlem1  47013  hspmbllem2  47070  ovolval5lem3  47097  smfpimbor1lem1  47241  smfsuplem1  47254  smflimsuplem4  47266  sigarls  47300  cnambpcma  47757  elfzelfzlble  47784  submodaddmod  47810  difltmodne  47811  m1mod0mod1  47823  modmkpkne  47830  mod2addne  47833  modm2nep1  47835  modm1nep2  47837  modm1nem2  47838  fsumsplitsndif  47844  fundcmpsurinjALT  47887  iccpartiltu  47897  prproropf1olem2  47979  fmtno4prmfac  48050  2pwp1prmfmtno  48068  lighneallem4b  48087  nprmdvdsfacm1lem4  48101  mogoldbblem  48211  gbegt5  48252  sbgoldbm  48275  nnsum3primesle9  48285  nnsum4primesodd  48287  nnsum4primesoddALTV  48288  evengpoap3  48290  nnsum4primesevenALTV  48292  clnbgredg  48331  opstrgric  48417  clnbgrgrimlem  48424  grtrif1o  48433  isubgr3stgrlem1  48457  isubgr3stgrlem4  48460  gpgusgralem  48547  gpg3nbgrvtx0  48567  isupwlk  48627  lidldomnnring  48727  2zrngacmnd  48739  rhmsubcALTVlem2  48773  fprmappr  48836  zlmodzxzscm  48848  gsumlsscl  48871  lincvalsng  48907  lincvalpr  48909  lincdifsn  48915  linc1  48916  lincellss  48917  fdivmpt  49031  digexp  49098  2arymaptfo  49145  line  49223  rrxline  49225  itsclc0xyqsolr  49260  iscnrm3r  49438  resipos  49465  amgmwlem  50292