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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 1088

This theorem is referenced by:  3ad2ant2  1134  3ad2ant3  1135  3simpc  1150  eupickb  2630  spc3egv  3558  sbciegftOLD  3779  reuhyp  5358  predtrss  6269  onunel  6413  funopg  6515  funprg  6535  funtpg  6536  funcnvtp  6544  unima  6897  fvun1  6913  fnreseql  6981  xpprsng  7073  ftpg  7089  f1ounsn  7206  f13dfv  7208  f1ocoima  7237  f1ofvswap  7240  mpoeq3ia  7424  ordunel  7757  fex2  7866  funexw  7884  poxp  8058  poxp2  8073  poxp3  8080  poseq  8088  suppval1  8096  wfr3g  8249  smores3  8273  oaord  8462  oacan  8463  oaword  8464  omord  8483  omcan  8484  omwordri  8487  odi  8494  omass  8495  oeord  8503  oecan  8504  oewordri  8507  oeordsuc  8509  nnaord  8534  nnaordr  8535  nndi  8538  nnmass  8539  nnaword  8542  nnmord  8547  nnmwordri  8551  naddelim  8601  naddel1  8602  naddel2  8603  naddss1  8604  naddss2  8605  naddasslem2  8610  nadd32  8612  erov  8738  ecopovtrn  8744  ixpf  8844  f1oen4g  8887  f1dom4g  8888  mapxpen  9056  ssfi  9082  sbthfilem  9107  sbthfi  9108  onomeneq  9123  fimax2g  9170  unbnn  9180  funisfsupp  9251  inelfi  9302  elfiun  9314  sup0  9351  suppr  9356  infpr  9389  ttrclss  9610  frr3g  9649  r111  9668  dif1card  9901  ackbij1lem16  10125  cff1  10149  cfflb  10150  cfsmolem  10161  fin23lem34  10237  hsmexlem2  10318  axcc3  10329  domtriomlem  10333  axdc3lem4  10344  axdc4lem  10346  axcclem  10348  konigthlem  10459  gchdomtri  10520  tskpr  10661  tskop  10662  tskuni  10674  tskun  10677  gruop  10696  gruun  10697  grudomon  10708  adderpqlem  10845  mulerpqlem  10846  addassnq  10849  mulassnq  10850  distrnq  10852  ltsonq  10860  ltanq  10862  ltmnq  10863  genpass  10900  distrlem1pr  10916  distrlem4pr  10917  ltsopr  10923  adddir  11103  axlttrn  11185  ltletr  11205  letr  11207  mul32  11279  mul31  11280  add32  11332  subsub23  11365  addsubass  11370  subcan2  11386  subsub2  11389  nppcan2  11392  sub32  11395  nnncan  11396  nnncan2  11398  pnpcan2  11401  subdi  11550  subdir  11551  receu  11762  mulcan1g  11770  mulcan2g  11771  divmul3  11781  divrec  11792  divrec2  11793  div11  11804  divsubdir  11815  subdivcomb2  11817  divdiv1  11832  redivcl  11840  div2neg  11844  ltmul2  11972  lemul1  11973  lemul2  11974  lemul2a  11976  lediv1  11987  gt0div  11988  ge0div  11989  mulsuble0b  11994  ltdivmul  11997  ledivmul  11998  ltdivmul2  11999  ledivmul2  12001  lemuldiv  12002  ltdiv23  12013  lediv23  12014  ledivp1i  12047  ltdivp1i  12048  uzind2  12566  nn0ind  12568  fnn0ind  12572  uz3m2nn  12792  xrltletr  13056  xrletr  13057  xrre2  13069  xrltmin  13081  xrlemin  13083  xleadd2a  13153  xleadd1  13154  xltadd2  13156  xmulasslem3  13185  xmulass  13186  xltmul2  13192  ixxdisj  13260  iooneg  13371  iccneg  13372  icoshft  13373  icoshftf1o  13374  icodisj  13376  snunioo  13378  fzen  13441  ssfzunsnext  13469  fzrev3  13490  2ffzeq  13549  fzoaddel2  13620  elfzodifsumelfzo  13631  ssfzoulel  13660  ssfzo12bi  13661  fzoopth  13662  fzoshftral  13687  adddivflid  13722  flltdivnn0lt  13737  ltdifltdiv  13738  fldiv4p1lem1div2  13739  modcyc  13810  modcyc2  13811  modaddabs  13815  muladdmod  13819  modsubmodmod  13837  modaddmodup  13841  modaddmulmod  13845  moddi  13846  modsubdir  13847  expdiv  14020  digit2  14143  nfile  14266  hashdifpr  14322  hashgt23el  14331  hashreshashfun  14346  hashf1dmcdm  14351  hash3tpexb  14401  fi1uzind  14414  ccatval1  14484  ccatass  14496  swrdval  14551  swrdnd  14562  swrd0  14566  swrdfv2  14569  pfxsuff1eqwrdeq  14606  swrdswrdlem  14611  pfxccatin12lem2a  14634  pfxccatin12lem1  14635  repswccat  14693  cshwidxmod  14710  cshwidxmodr  14711  cshf1  14717  repswcshw  14719  2cshw  14720  2cshwcom  14723  2cshwcshw  14732  cshwcsh2id  14735  ccatco  14742  2swrd2eqwrdeq  14860  wwlktovf  14863  brcnvtrclfv  14910  shftval2  14982  mulre  15028  absdiv  15202  absdiflt  15225  absdifle  15226  abs3dif  15239  cau3  15263  ello12r  15424  elo12r  15435  modfsummods  15700  geoisum1c  15787  rpnnen2lem4  16126  rpnnen2lem7  16129  addmulmodb  16176  dvdsmulc  16194  dvdsmulcr  16196  dvdsmultr1  16207  dvdsmultr2  16209  dvdssub2  16212  oexpneg  16256  divalgb  16315  ndvdsadd  16321  sadass  16382  modgcd  16443  dvdsgcd  16455  dvdsgcdb  16456  gcdass  16458  mulgcd  16459  absmulgcd  16460  rpmulgcd  16468  expgcd  16474  zexpgcd  16476  nn0seqcvgd  16481  algcvga  16490  lcmdvdsb  16524  lcmass  16525  lcmfunsnlem1  16548  lcmfunsnlem2lem1  16549  lcmfunsnlem2lem2  16550  coprmdvds  16564  coprmdvds2  16565  rpmul  16570  cncongr1  16578  cncongr2  16579  qnumdenbi  16655  modprm0  16717  coprimeprodsq  16720  pythagtriplem4  16731  pythagtriplem8  16735  pythagtriplem9  16736  pythagtriplem12  16738  pythagtriplem14  16740  pythagtriplem16  16742  pcpremul  16755  pcgcd  16790  vdwapval  16885  vdwapun  16886  prmgaplem3  16965  prmgaplem4  16966  prmgaplem7  16969  prmgapprmolem  16973  mreiincl  17498  mreincl  17501  mremre  17506  mrcss  17522  catcisolem  18017  pleval2  18241  pospo  18249  latlem  18343  latjcom  18353  latmcom  18369  lubss  18419  lubun  18421  clatglbss  18425  ipole  18440  ipolt  18441  pslem  18478  dirtr  18508  gsumsgrpccat  18748  gsumws2  18750  frmdmnd  18767  symggrplem  18792  isgrpi  18872  grpsubrcan  18934  grpinvsub  18935  grpsubeq0  18939  grpsubadd0sub  18940  grpnpcan  18945  qussub  19104  ghmsub  19137  symgpssefmnd  19309  symggrp  19313  symgextsymg  19337  gsmsymgreqlem2  19344  symgfixfolem1  19351  pmtrprfv3  19367  symggen  19383  lsmass  19582  efgsrel  19647  cntzcmn  19753  dvrcl  20323  unitdvcl  20324  dvrcan1  20328  subrngmre  20478  subrgmre  20513  rhmsubclem2  20602  rrgeq0  20616  abvsubtri  20743  abvtrivd  20748  lmodvsubval2  20851  rmodislmodlem  20863  rmodislmod  20864  lss0cl  20881  lssintcl  20898  lssincl  20899  reslmhm2  20988  lspvadd  21031  lspsntrim  21033  islbs3  21093  rnglidlmmgm  21183  cncrng  21326  cncrngOLD  21327  xrsmcmn  21329  cndrng  21336  cndrngOLD  21337  cnsrng  21343  absabv  21362  xrs1mnd  21378  psgnco  21521  zrhpsgninv  21523  zrhpsgnevpm  21529  zrhpsgnodpm  21530  zrhpsgnelbas  21532  zrhcopsgnelbas  21533  uvcresum  21731  lindfmm  21765  lindsmm  21766  evlsval2  22023  mamudm  22311  mamufacex  22312  matsubgcell  22350  matsc  22366  scmatscmide  22423  scmatrhmcl  22444  1marepvsma1  22499  m1detdiag  22513  mdetralt  22524  m2detleiblem7  22543  gsummatr01lem3  22573  gsummatr01  22575  smadiadetlem0  22577  decpmate  22682  decpmatcl  22683  pm2mpcl  22713  pm2mpghmlem2  22728  chfacfscmul0  22774  chfacfscmulgsum  22776  chfacfpmmul0  22778  chfacfpmmulgsum  22780  unopn  22819  clsss  22970  cldmre  22994  toponmre  23009  opnssneib  23031  restabs  23081  restcls  23097  restntr  23098  hausnei2  23269  cmpsublem  23315  bwth  23326  hausmapdom  23416  ptpjcn  23527  upxp  23539  ptrescn  23555  xkopjcn  23572  fbssfi  23753  snfil  23780  ufprim  23825  rnelfm  23869  flimrest  23899  fclsrest  23940  tmdgsum  24011  blpnfctr  24352  mscl  24377  xmscl  24378  xmsge0  24379  xmseq0  24380  restmetu  24486  ngpds  24520  tngngp3  24572  unitnmn0  24584  xrsxmet  24726  metds0  24767  mpomulcn  24786  cncfmptc  24833  isclmp  25025  cnlmod  25068  ncvsi  25079  cphsqrtcl  25112  cfil3i  25197  cfilres  25224  cmssmscld  25278  cmmbl  25463  voliunlem2  25480  itg2ub  25662  itgrecl  25727  r1pid  26094  eflogeq  26539  cxpadd  26616  cxpcom  26676  logbchbase  26709  relogbreexp  26713  relogbzexp  26714  relogbmulexp  26716  logbleb  26721  logblt  26722  lawcos  26754  pythag  26755  asinsinb  26835  acoscosb  26836  atantanb  26862  amgmlem  26928  lgsneg  27260  lgsne0  27274  lgsmodeq  27281  lgsmulsqcoprm  27282  gausslemma2dlem1a  27304  2sqreulem2  27391  sltres  27602  noetainflem1  27677  sltletr  27696  sletr  27698  nocvxmin  27719  madebdaylemold  27844  lrrecpo  27885  sltadd2im  27930  sleadd1im  27931  sleadd2im  27932  sleadd1  27933  sleadd2  27934  sltadd1  27936  addscan2  27937  addscan1  27938  subadds  28011  sltsub1  28017  divscl  28162  onscutlt  28202  zsoring  28333  expscllem  28354  0reno  28400  brbtwn2  28884  colinearalg  28889  eleesubd  28891  axcgrrflx  28893  axcgrtr  28894  axsegcon  28906  ax5seglem1  28907  ax5seglem2  28908  ax5seglem4  28911  axbtwnid  28918  axlowdimlem14  28934  axlowdim  28940  axcontlem5  28947  axcontlem7  28949  nb3grprlem2  29360  cplgr3v  29414  cusgrsizeindslem  29431  sizusglecusglem2  29442  umgr2v2e  29505  cusgrrusgr  29561  iswlk  29590  edginwlk  29614  uspgr2wlkeq  29625  uspgr2wlkeq2  29626  uspgr2wlkeqi  29627  wlkonprop  29636  wlkon2n0  29644  pthdadjvtx  29707  upgr2pthnlp  29711  spthonepeq  29731  pthdlem2lem  29746  crctcshwlkn0lem3  29791  crctcshwlkn0lem5  29793  wlkiswwlks2lem4  29851  wlkiswwlks2lem6  29853  wlklnwwlkln2lem  29861  wwlksnred  29871  wwlksnextbi  29873  wwlksnextwrd  29876  2pthdlem1  29909  2wlkdlem10  29914  umgr2adedgwlkonALT  29926  elwwlks2s3  29930  elwwlks2ons3im  29933  s3wwlks2on  29935  2wspdisj  29941  2wspiundisj  29942  clwwlkgt0  29964  clwlkclwwlklem2a4  29975  clwlkclwwlklem2a  29976  clwlkclwwlk  29980  clwlkclwwlk2  29981  clwlkclwwlkfo  29987  clwwisshclwwslemlem  29991  erclwwlktr  30000  clwwlkf  30025  wwlksubclwwlk  30036  erclwwlkntr  30049  clwwlknon  30068  frcond1  30244  frgr3v  30253  3vfriswmgr  30256  frgrwopreglem4a  30288  frrusgrord0lem  30317  clwwnonrepclwwnon  30323  extwwlkfab  30330  numclwwlk1lem2f1  30335  numclwwlk1lem2fo  30336  clwlknon2num  30346  numclwwlk2lem1  30354  numclwlk2lem2f  30355  numclwlk2lem2f1o  30357  numclwwlk2  30359  frgrreggt1  30371  friendshipgt3  30376  imsmetlem  30668  nmoxr  30744  nmoolb  30749  blometi  30781  phpar2  30801  phpar  30802  ipasslem5  30813  hvadd32  31012  hvaddsub12  31016  hvaddsubass  31019  hvsubass  31022  hvsub32  31023  hvsubdistr1  31027  hvsubdistr2  31028  hvmulcan  31050  hvmulcan2  31051  hvsubcan  31052  his5  31064  his2sub  31070  hhssabloilem  31239  hhssnv  31242  shlej2  31339  pjoi0  31695  hodcl  31725  hoadd32  31761  hosubdi  31786  hosubsub2  31790  hoaddsubass  31793  hosubsub4  31796  nmoplb  31885  unop  31893  hmop  31900  nmfnlb  31902  lnopmul  31945  kbass1  32094  kbass2  32095  leopmul2i  32113  leoptr  32115  cvntr  32270  mdslmd4i  32311  mdexchi  32313  atcv1  32358  sumdmdii  32393  fcoinvbr  32583  fpwrelmapffs  32715  xreceu  32900  isinftm  33148  unitdivcld  33912  esummulc1  34092  hasheuni  34096  unelsiga  34145  inelpisys  34165  carsgsigalem  34326  signswmnd  34568  bnj545  34905  bnj594  34922  bnj1311  35034  fissorduni  35099  r1filimi  35112  fineqvac  35137  fineqvnttrclselem3  35141  usgrgt2cycl  35172  subgrwlk  35174  acycgr1v  35191  cvmsf1o  35314  cvmscld  35315  satefvfmla1  35467  elnanelprv  35471  lediv2aALT  35719  gcd32  35791  fununiq  35811  dfrdg4  35991  brcolinear  36099  colinearex  36100  nn0prpwlem  36362  clsun  36368  fnemeet1  36406  fnemeet2  36407  fnejoin1  36408  fnejoin2  36409  eltail  36414  rdgeqoa  37410  nlpineqsn  37448  curf  37644  lindsadd  37659  poimirlem28  37694  cnambfre  37714  ftc1anclem4  37742  cocanfo  37765  f1ocan1fv  37772  metf1o  37801  ismtybnd  37853  ghomco  37937  isdrngo2  38004  inidl  38076  igenmin  38110  brxrn  38408  brredunds  38669  cmtvalN  39256  cvrval  39314  pmapmeet  39818  paddval  39843  paddssat  39859  elpcliN  39938  pclssN  39939  pclunN  39943  paddunN  39972  poldmj1N  39973  tendoplcl2  40823  tendoplcl  40826  dihmeet  41388  lcmineqlem1  42068  reltsub1  42425  reltsubadd2  42426  resubsub4  42428  reppncan  42432  resubdi  42435  readdcan2  42452  subresre  42470  mapco2g  42753  mzpcompact2lem  42790  eqrabdioph  42816  lerabdioph  42844  eluzrabdioph  42845  ltrabdioph  42847  nerabdioph  42848  dvdsrabdioph  42849  reglogcl  42929  rmxyadd  42960  rmyabs  42997  congadd  43005  congabseq  43013  rmydioph  43053  mendring  43227  mendlmod  43228  iocinico  43251  omge1  43336  relexp0a  43755  relexpaddss  43757  brcoffn  44069  ismnushort  44340  dvconstbi  44373  uzwo4  45096  ssin0  45098  ssinc  45130  ssdec  45131  fvmpt2bd  45213  disjf1o  45234  ssnnf1octb  45237  sub31  45337  fperiodmullem  45350  ssfiunibd  45356  infxr  45411  fmul01  45626  islptre  45665  lptre2pt  45684  limcleqr  45688  limclner  45695  limsuppnflem  45754  limsupvaluz2  45782  supcnvlimsup  45784  xlimmnfvlem2  45877  xlimmnfv  45878  xlimpnfvlem2  45881  xlimpnfv  45882  climxlim2lem  45889  coskpi2  45910  cosknegpi  45913  dvnmptdivc  45982  dvdsn1add  45983  dvnmptconst  45985  dvmptfprod  45989  dvnprodlem1  45990  dvnprodlem2  45991  ovolsplit  46032  stoweidlem60  46104  stowei  46108  dirkeritg  46146  fourierdlem70  46220  fourierdlem71  46221  fourierdlem103  46253  fourierdlem104  46254  fouriersw  46275  rrxtopnfi  46331  saluncl  46361  salexct  46378  sge0ltfirp  46444  sge0iunmpt  46462  meadjiunlem  46509  meaiuninc3v  46528  carageniuncllem1  46565  caratheodorylem1  46570  ovncvrrp  46608  ovnsubaddlem1  46614  hspmbllem2  46671  ovolval5lem3  46698  smfpimbor1lem1  46842  smfsuplem1  46855  smflimsuplem4  46867  sigarls  46901  cnambpcma  47331  elfzelfzlble  47358  submodaddmod  47378  difltmodne  47379  m1mod0mod1  47391  modmkpkne  47398  mod2addne  47401  modm2nep1  47403  modm1nep2  47405  modm1nem2  47406  fsumsplitsndif  47410  fundcmpsurinjALT  47449  iccpartiltu  47459  prproropf1olem2  47541  fmtno4prmfac  47609  2pwp1prmfmtno  47627  lighneallem4b  47646  mogoldbblem  47757  gbegt5  47798  sbgoldbm  47821  nnsum3primesle9  47831  nnsum4primesodd  47833  nnsum4primesoddALTV  47834  evengpoap3  47836  nnsum4primesevenALTV  47838  clnbgredg  47877  opstrgric  47963  clnbgrgrimlem  47970  grtrif1o  47979  isubgr3stgrlem1  48003  isubgr3stgrlem4  48006  gpgusgralem  48093  gpg3nbgrvtx0  48113  isupwlk  48173  lidldomnnring  48273  2zrngacmnd  48285  rhmsubcALTVlem2  48319  fprmappr  48382  zlmodzxzscm  48394  gsumlsscl  48417  lincvalsng  48454  lincvalpr  48456  lincdifsn  48462  linc1  48463  lincellss  48464  fdivmpt  48578  digexp  48645  2arymaptfo  48692  line  48770  rrxline  48772  itsclc0xyqsolr  48807  iscnrm3r  48985  resipos  49012  amgmwlem  49840