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  2634  spc3egv  3582  sbciegftOLD  3803  reuhyp  5390  predtrss  6311  onunel  6458  funopg  6569  funprg  6589  funtpg  6590  funcnvtp  6598  unima  6953  fvun1  6969  fnreseql  7037  xpprsng  7129  ftpg  7145  f1ounsn  7264  f13dfv  7266  f1ocoima  7295  f1ofvswap  7298  mpoeq3ia  7483  ordunel  7819  fex2  7930  funexw  7948  poxp  8125  poxp2  8140  poxp3  8147  poseq  8155  suppval1  8163  wfr3g  8319  smores3  8365  oaord  8557  oacan  8558  oaword  8559  omord  8578  omcan  8579  omwordri  8582  odi  8589  omass  8590  oeord  8598  oecan  8599  oewordri  8602  oeordsuc  8604  nnaord  8629  nnaordr  8630  nndi  8633  nnmass  8634  nnaword  8637  nnmord  8642  nnmwordri  8646  naddelim  8696  naddel1  8697  naddel2  8698  naddss1  8699  naddss2  8700  naddasslem2  8705  nadd32  8707  erov  8826  ecopovtrn  8832  ixpf  8932  f1oen4g  8977  f1dom4g  8978  mapxpen  9155  dif1enlemOLD  9169  ssfi  9185  sbthfilem  9210  sbthfi  9211  onomeneq  9235  fimax2g  9292  unbnn  9302  funisfsupp  9377  inelfi  9428  elfiun  9440  sup0  9477  suppr  9482  infpr  9515  ttrclss  9732  frr3g  9768  r111  9787  dif1card  10022  ackbij1lem16  10246  cff1  10270  cfflb  10271  cfsmolem  10282  fin23lem34  10358  hsmexlem2  10439  axcc3  10450  domtriomlem  10454  axdc3lem4  10465  axdc4lem  10467  axcclem  10469  konigthlem  10580  gchdomtri  10641  tskpr  10782  tskop  10783  tskuni  10795  tskun  10798  gruop  10817  gruun  10818  grudomon  10829  adderpqlem  10966  mulerpqlem  10967  addassnq  10970  mulassnq  10971  distrnq  10973  ltsonq  10981  ltanq  10983  ltmnq  10984  genpass  11021  distrlem1pr  11037  distrlem4pr  11038  ltsopr  11044  adddir  11224  axlttrn  11305  ltletr  11325  letr  11327  mul32  11399  mul31  11400  add32  11452  subsub23  11485  addsubass  11490  subcan2  11506  subsub2  11509  nppcan2  11512  sub32  11515  nnncan  11516  nnncan2  11518  pnpcan2  11521  subdi  11668  subdir  11669  receu  11880  mulcan1g  11888  mulcan2g  11889  divmul3  11899  divrec  11910  divrec2  11911  div11  11922  divsubdir  11933  subdivcomb2  11935  divdiv1  11950  redivcl  11958  div2neg  11962  ltmul2  12090  lemul1  12091  lemul2  12092  lemul2a  12094  lediv1  12105  gt0div  12106  ge0div  12107  mulsuble0b  12112  ltdivmul  12115  ledivmul  12116  ltdivmul2  12117  ledivmul2  12119  lemuldiv  12120  ltdiv23  12131  lediv23  12132  ledivp1i  12165  ltdivp1i  12166  uzind2  12684  nn0ind  12686  fnn0ind  12690  uz3m2nn  12905  xrltletr  13171  xrletr  13172  xrre2  13184  xrltmin  13196  xrlemin  13198  xleadd2a  13268  xleadd1  13269  xltadd2  13271  xmulasslem3  13300  xmulass  13301  xltmul2  13307  ixxdisj  13375  iooneg  13486  iccneg  13487  icoshft  13488  icoshftf1o  13489  icodisj  13491  snunioo  13493  fzen  13556  ssfzunsnext  13584  fzrev3  13605  2ffzeq  13664  fzoaddel2  13734  elfzodifsumelfzo  13745  ssfzoulel  13774  ssfzo12bi  13775  fzoopth  13776  fzoshftral  13798  adddivflid  13833  flltdivnn0lt  13848  ltdifltdiv  13849  fldiv4p1lem1div2  13850  modcyc  13921  modcyc2  13922  modaddabs  13924  muladdmod  13928  modsubmodmod  13946  modaddmodup  13950  modaddmulmod  13954  moddi  13955  modsubdir  13956  expdiv  14129  digit2  14252  nfile  14375  hashdifpr  14431  hashgt23el  14440  hashreshashfun  14455  hashf1dmcdm  14460  hash3tpexb  14510  fi1uzind  14523  ccatval1  14593  ccatass  14604  swrdval  14659  swrdnd  14670  swrd0  14674  swrdfv2  14677  pfxsuff1eqwrdeq  14715  swrdswrdlem  14720  pfxccatin12lem2a  14743  pfxccatin12lem1  14744  repswccat  14802  cshwidxmod  14819  cshwidxmodr  14820  cshf1  14826  repswcshw  14828  2cshw  14829  2cshwcom  14832  2cshwcshw  14842  cshwcsh2id  14845  ccatco  14852  2swrd2eqwrdeq  14970  wwlktovf  14973  brcnvtrclfv  15020  shftval2  15092  mulre  15138  absdiv  15312  absdiflt  15334  absdifle  15335  abs3dif  15348  cau3  15372  ello12r  15531  elo12r  15542  modfsummods  15807  geoisum1c  15894  rpnnen2lem4  16233  rpnnen2lem7  16236  addmulmodb  16283  dvdsmulc  16301  dvdsmulcr  16303  dvdsmultr1  16313  dvdsmultr2  16315  dvdssub2  16318  oexpneg  16362  divalgb  16421  ndvdsadd  16427  sadass  16488  modgcd  16549  dvdsgcd  16561  dvdsgcdb  16562  gcdass  16564  mulgcd  16565  absmulgcd  16566  rpmulgcd  16574  expgcd  16580  zexpgcd  16582  nn0seqcvgd  16587  algcvga  16596  lcmdvdsb  16630  lcmass  16631  lcmfunsnlem1  16654  lcmfunsnlem2lem1  16655  lcmfunsnlem2lem2  16656  coprmdvds  16670  coprmdvds2  16671  rpmul  16676  cncongr1  16684  cncongr2  16685  qnumdenbi  16761  modprm0  16823  coprimeprodsq  16826  pythagtriplem4  16837  pythagtriplem8  16841  pythagtriplem9  16842  pythagtriplem12  16844  pythagtriplem14  16846  pythagtriplem16  16848  pcpremul  16861  pcgcd  16896  vdwapval  16991  vdwapun  16992  prmgaplem3  17071  prmgaplem4  17072  prmgaplem7  17075  prmgapprmolem  17079  mreiincl  17606  mreincl  17609  mremre  17614  mrcss  17626  catcisolem  18121  pleval2  18345  pospo  18353  latlem  18445  latjcom  18455  latmcom  18471  lubss  18521  lubun  18523  clatglbss  18527  ipole  18542  ipolt  18543  pslem  18580  dirtr  18610  gsumsgrpccat  18816  gsumws2  18818  frmdmnd  18835  symggrplem  18860  isgrpi  18940  grpsubrcan  19002  grpinvsub  19003  grpsubeq0  19007  grpsubadd0sub  19008  grpnpcan  19013  qussub  19172  ghmsub  19205  symgpssefmnd  19375  symggrp  19379  symgextsymg  19403  gsmsymgreqlem2  19410  symgfixfolem1  19417  pmtrprfv3  19433  symggen  19449  lsmass  19648  efgsrel  19713  cntzcmn  19819  dvrcl  20362  unitdvcl  20363  dvrcan1  20367  subrngmre  20520  subrgmre  20555  rhmsubclem2  20644  rrgeq0  20658  abvsubtri  20785  abvtrivd  20790  lmodvsubval2  20872  rmodislmodlem  20884  rmodislmod  20885  lss0cl  20902  lssintcl  20919  lssincl  20920  reslmhm2  21009  lspvadd  21052  lspsntrim  21054  islbs3  21114  rnglidlmmgm  21204  cncrng  21349  cncrngOLD  21350  xrsmcmn  21352  cndrng  21359  cndrngOLD  21360  cnsrng  21366  xrs1mnd  21370  absabv  21390  psgnco  21541  zrhpsgninv  21543  zrhpsgnevpm  21549  zrhpsgnodpm  21550  zrhpsgnelbas  21552  zrhcopsgnelbas  21553  uvcresum  21751  lindfmm  21785  lindsmm  21786  evlsval2  22043  mamudm  22331  mamufacex  22332  matsubgcell  22370  matsc  22386  scmatscmide  22443  scmatrhmcl  22464  1marepvsma1  22519  m1detdiag  22533  mdetralt  22544  m2detleiblem7  22563  gsummatr01lem3  22593  gsummatr01  22595  smadiadetlem0  22597  decpmate  22702  decpmatcl  22703  pm2mpcl  22733  pm2mpghmlem2  22748  chfacfscmul0  22794  chfacfscmulgsum  22796  chfacfpmmul0  22798  chfacfpmmulgsum  22800  unopn  22839  clsss  22990  cldmre  23014  toponmre  23029  opnssneib  23051  restabs  23101  restcls  23117  restntr  23118  hausnei2  23289  cmpsublem  23335  bwth  23346  hausmapdom  23436  ptpjcn  23547  upxp  23559  ptrescn  23575  xkopjcn  23592  fbssfi  23773  snfil  23800  ufprim  23845  rnelfm  23889  flimrest  23919  fclsrest  23960  tmdgsum  24031  blpnfctr  24373  mscl  24398  xmscl  24399  xmsge0  24400  xmseq0  24401  restmetu  24507  ngpds  24541  tngngp3  24593  unitnmn0  24605  xrsxmet  24747  metds0  24788  mpomulcn  24807  cncfmptc  24854  isclmp  25046  cnlmod  25089  ncvsi  25101  cphsqrtcl  25134  cfil3i  25219  cfilres  25246  cmssmscld  25300  cmmbl  25485  voliunlem2  25502  itg2ub  25684  itgrecl  25749  r1pid  26116  eflogeq  26561  cxpadd  26638  cxpcom  26698  logbchbase  26731  relogbreexp  26735  relogbzexp  26736  relogbmulexp  26738  logbleb  26743  logblt  26744  lawcos  26776  pythag  26777  asinsinb  26857  acoscosb  26858  atantanb  26884  amgmlem  26950  lgsneg  27282  lgsne0  27296  lgsmodeq  27303  lgsmulsqcoprm  27304  gausslemma2dlem1a  27326  2sqreulem2  27413  sltres  27624  noetainflem1  27699  sltletr  27718  sletr  27720  nocvxmin  27740  madebdaylemold  27853  lrrecpo  27891  sltadd2im  27936  sleadd1im  27937  sleadd2im  27938  sleadd1  27939  sleadd2  27940  sltadd1  27942  addscan2  27943  addscan1  27944  subadds  28017  sltsub1  28023  divscl  28164  nohalf  28324  0reno  28346  brbtwn2  28830  colinearalg  28835  eleesubd  28837  axcgrrflx  28839  axcgrtr  28840  axsegcon  28852  ax5seglem1  28853  ax5seglem2  28854  ax5seglem4  28857  axbtwnid  28864  axlowdimlem14  28880  axlowdim  28886  axcontlem5  28893  axcontlem7  28895  nb3grprlem2  29306  cplgr3v  29360  cusgrsizeindslem  29377  sizusglecusglem2  29388  umgr2v2e  29451  cusgrrusgr  29507  iswlk  29536  edginwlk  29561  uspgr2wlkeq  29572  uspgr2wlkeq2  29573  uspgr2wlkeqi  29574  wlkonprop  29584  wlkon2n0  29592  pthdadjvtx  29656  upgr2pthnlp  29660  spthonepeq  29680  pthdlem2lem  29695  crctcshwlkn0lem3  29740  crctcshwlkn0lem5  29742  wlkiswwlks2lem4  29800  wlkiswwlks2lem6  29802  wlklnwwlkln2lem  29810  wwlksnred  29820  wwlksnextbi  29822  wwlksnextwrd  29825  2pthdlem1  29858  2wlkdlem10  29863  umgr2adedgwlkonALT  29875  elwwlks2s3  29879  elwwlks2ons3im  29882  s3wwlks2on  29884  2wspdisj  29890  2wspiundisj  29891  clwwlkgt0  29913  clwlkclwwlklem2a4  29924  clwlkclwwlklem2a  29925  clwlkclwwlk  29929  clwlkclwwlk2  29930  clwlkclwwlkfo  29936  clwwisshclwwslemlem  29940  erclwwlktr  29949  clwwlkf  29974  wwlksubclwwlk  29985  erclwwlkntr  29998  clwwlknon  30017  frcond1  30193  frgr3v  30202  3vfriswmgr  30205  frgrwopreglem4a  30237  frrusgrord0lem  30266  clwwnonrepclwwnon  30272  extwwlkfab  30279  numclwwlk1lem2f1  30284  numclwwlk1lem2fo  30285  clwlknon2num  30295  numclwwlk2lem1  30303  numclwlk2lem2f  30304  numclwlk2lem2f1o  30306  numclwwlk2  30308  frgrreggt1  30320  friendshipgt3  30325  imsmetlem  30617  nmoxr  30693  nmoolb  30698  blometi  30730  phpar2  30750  phpar  30751  ipasslem5  30762  hvadd32  30961  hvaddsub12  30965  hvaddsubass  30968  hvsubass  30971  hvsub32  30972  hvsubdistr1  30976  hvsubdistr2  30977  hvmulcan  30999  hvmulcan2  31000  hvsubcan  31001  his5  31013  his2sub  31019  hhssabloilem  31188  hhssnv  31191  shlej2  31288  pjoi0  31644  hodcl  31674  hoadd32  31710  hosubdi  31735  hosubsub2  31739  hoaddsubass  31742  hosubsub4  31745  nmoplb  31834  unop  31842  hmop  31849  nmfnlb  31851  lnopmul  31894  kbass1  32043  kbass2  32044  leopmul2i  32062  leoptr  32064  cvntr  32219  mdslmd4i  32260  mdexchi  32262  atcv1  32307  sumdmdii  32342  fcoinvbr  32532  fpwrelmapffs  32657  xreceu  32842  isinftm  33125  unitdivcld  33878  esummulc1  34058  hasheuni  34062  unelsiga  34111  inelpisys  34131  carsgsigalem  34293  signswmnd  34535  bnj545  34872  bnj594  34889  bnj1311  35001  fineqvac  35074  usgrgt2cycl  35098  subgrwlk  35100  acycgr1v  35117  cvmsf1o  35240  cvmscld  35241  satefvfmla1  35393  elnanelprv  35397  lediv2aALT  35645  gcd32  35712  fununiq  35732  dfrdg4  35915  brcolinear  36023  colinearex  36024  nn0prpwlem  36286  clsun  36292  fnemeet1  36330  fnemeet2  36331  fnejoin1  36332  fnejoin2  36333  eltail  36338  rdgeqoa  37334  nlpineqsn  37372  curf  37568  lindsadd  37583  poimirlem28  37618  cnambfre  37638  ftc1anclem4  37666  cocanfo  37689  f1ocan1fv  37696  metf1o  37725  ismtybnd  37777  ghomco  37861  isdrngo2  37928  inidl  38000  igenmin  38034  brxrn  38338  brredunds  38590  cmtvalN  39175  cvrval  39233  pmapmeet  39738  paddval  39763  paddssat  39779  elpcliN  39858  pclssN  39859  pclunN  39863  paddunN  39892  poldmj1N  39893  tendoplcl2  40743  tendoplcl  40746  dihmeet  41308  lcmineqlem1  41988  factwoffsmonot  42201  reltsub1  42376  reltsubadd2  42377  resubsub4  42379  reppncan  42383  resubdi  42386  readdcan2  42402  subresre  42420  mapco2g  42684  mzpcompact2lem  42721  eqrabdioph  42747  lerabdioph  42775  eluzrabdioph  42776  ltrabdioph  42778  nerabdioph  42779  dvdsrabdioph  42780  reglogcl  42860  rmxyadd  42892  rmyabs  42929  congadd  42937  congabseq  42945  rmydioph  42985  mendring  43159  mendlmod  43160  iocinico  43183  omge1  43268  relexp0a  43687  relexpaddss  43689  brcoffn  44001  ismnushort  44273  dvconstbi  44306  uzwo4  45025  ssin0  45027  ssinc  45059  ssdec  45060  fvmpt2bd  45142  disjf1o  45163  ssnnf1octb  45166  sub31  45267  fperiodmullem  45280  ssfiunibd  45286  infxr  45342  fmul01  45557  islptre  45596  lptre2pt  45617  limcleqr  45621  limclner  45628  limsuppnflem  45687  limsupvaluz2  45715  supcnvlimsup  45717  xlimmnfvlem2  45810  xlimmnfv  45811  xlimpnfvlem2  45814  xlimpnfv  45815  climxlim2lem  45822  coskpi2  45843  cosknegpi  45846  dvnmptdivc  45915  dvdsn1add  45916  dvnmptconst  45918  dvmptfprod  45922  dvnprodlem1  45923  dvnprodlem2  45924  ovolsplit  45965  stoweidlem60  46037  stowei  46041  dirkeritg  46079  fourierdlem70  46153  fourierdlem71  46154  fourierdlem103  46186  fourierdlem104  46187  fouriersw  46208  rrxtopnfi  46264  saluncl  46294  salexct  46311  sge0ltfirp  46377  sge0iunmpt  46395  meadjiunlem  46442  meaiuninc3v  46461  carageniuncllem1  46498  caratheodorylem1  46503  ovncvrrp  46541  ovnsubaddlem1  46547  hspmbllem2  46604  ovolval5lem3  46631  smfpimbor1lem1  46775  smfsuplem1  46788  smflimsuplem4  46800  sigarls  46834  cnambpcma  47271  elfzelfzlble  47298  submodaddmod  47318  difltmodne  47319  m1mod0mod1  47331  fsumsplitsndif  47335  fundcmpsurinjALT  47374  iccpartiltu  47384  prproropf1olem2  47466  fmtno4prmfac  47534  2pwp1prmfmtno  47552  lighneallem4b  47571  mogoldbblem  47682  gbegt5  47723  sbgoldbm  47746  nnsum3primesle9  47756  nnsum4primesodd  47758  nnsum4primesoddALTV  47759  evengpoap3  47761  nnsum4primesevenALTV  47763  clnbgredg  47801  opstrgric  47887  clnbgrgrimlem  47894  grtrif1o  47902  isubgr3stgrlem1  47926  isubgr3stgrlem4  47929  gpgusgralem  48008  gpg3nbgrvtx0  48026  isupwlk  48059  lidldomnnring  48159  2zrngacmnd  48171  rhmsubcALTVlem2  48205  fprmappr  48268  zlmodzxzscm  48280  gsumlsscl  48303  lincvalsng  48340  lincvalpr  48342  lincdifsn  48348  linc1  48349  lincellss  48350  difmodm1lt  48450  fdivmpt  48468  digexp  48535  2arymaptfo  48582  line  48660  rrxline  48662  itsclc0xyqsolr  48697  iscnrm3r  48870  resipos  48897  amgmwlem  49614