Theorem 3adant1 1148

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3ad2ant2  1152  3ad2ant3  1153  3simpc  1168  eupickb  2660  spc3egv  3557  rspc2ev  3588  reuhyp  5382  predtrss  6328  onunel  6473  fununiq  6560  funopg  6579  funprg  6599  funtpg  6600  funcnvtp  6608  unima  6965  fvun1  6981  fnreseql  7052  xpprsng  7147  ftpg  7165  f1ounsn  7284  f13dfv  7286  f1ocoima  7315  f1ofvswap  7318  mpoeq3ia  7502  ordunel  7842  fex2  7952  funexw  7968  poxp  8146  poxp2  8166  poxp3  8173  poseq  8181  suppval1  8190  wfr3g  8344  smores3  8368  oaord  8562  oacan  8563  oaword  8564  omord  8583  omcan  8584  omwordri  8587  odi  8594  omass  8595  oeord  8604  oecan  8605  oewordri  8608  oeordsuc  8610  nnaord  8635  nnaordr  8636  nndi  8639  nnmass  8640  nnaword  8643  nnmord  8648  nnmwordri  8652  naddelim  8703  naddel1  8704  naddel2  8705  naddss1  8706  naddss2  8707  naddasslem2  8712  nadd32  8714  erov  8842  ecopovtrn  8848  curf  8897  ixpf  8955  f1oen4g  8998  f1dom4g  8999  mapxpen  9169  ssfi  9195  sbthfilem  9220  sbthfi  9221  onomeneq  9236  fimax2g  9284  fissorduni  9289  unbnn  9295  funisfsupp  9366  inelfi  9417  elfiun  9429  sup0  9466  suppr  9471  infpr  9504  ttrclss  9728  frr3g  9767  r111  9789  r1filimi  9910  dif1card  10096  ackbij1lem16  10319  cff1  10343  cfflb  10344  cfsmolem  10355  fin23lem34  10431  hsmexlem2  10512  axcc3  10523  domtriomlem  10527  axdc3lem4  10538  axdc4lem  10540  axcclem  10542  konigthlem  10660  gchdomtri  10721  tskpr  10862  tskop  10863  tskuni  10875  tskun  10878  gruop  10897  gruun  10898  grudomon  10909  adderpqlem  11046  mulerpqlem  11047  addassnq  11050  mulassnq  11051  distrnq  11053  ltsonq  11061  ltanq  11063  ltmnq  11064  genpass  11101  distrlem1pr  11117  distrlem4pr  11118  ltsopr  11124  adddir  11304  axlttrn  11389  ltletr  11409  letr  11411  mul32  11483  mul31  11484  add32  11536  subsub23  11569  addsubass  11574  subcan2  11590  subsub2  11593  nppcan2  11596  sub32  11599  nnncan  11600  nnncan2  11602  pnpcan2  11605  subdi  11756  subdir  11757  receu  11968  mulcan1g  11976  mulcan2g  11977  divmul3  11986  divrec  11997  divrec2  11998  div11  12009  divsubdir  12017  subdivcomb2  12020  divdiv1  12035  redivcl  12043  div2neg  12047  ltmul2  12175  lemul1  12176  lemul2  12177  lemul2a  12179  lediv1  12189  gt0div  12190  ge0div  12191  mulsuble0b  12196  ltdivmul  12199  ledivmul  12200  ltdivmul2  12201  ledivmul2  12203  lemuldiv  12204  ltdiv23  12215  lediv23  12216  ledivp1i  12249  ltdivp1i  12250  uzind2  12799  nn0ind  12801  fnn0ind  12805  uz3m2nn  13028  xrltletr  13293  xrletr  13294  xrre2  13307  xrltmin  13319  xrlemin  13321  xleadd2a  13391  xleadd1  13392  xltadd2  13394  xmulasslem3  13423  xmulass  13424  xltmul2  13430  ixxdisj  13498  iooneg  13609  iccneg  13610  icoshft  13611  icoshftf1o  13612  icodisj  13614  snunioo  13616  fzen  13681  ssfzunsnext  13710  fzrev3  13731  2ffzeq  13790  fzoaddel2  13862  elfzodifsumelfzo  13873  ssfzoulel  13902  ssfzo12bi  13903  fzoopth  13904  fzoshftral  13929  adddivflid  13965  flltdivnn0lt  13980  ltdifltdiv  13981  fldiv4p1lem1div2  13982  modcyc  14053  modcyc2  14054  modaddabs  14058  muladdmod  14062  modsubmodmod  14080  modaddmodup  14084  modaddmulmod  14088  moddi  14089  modsubdir  14090  expdiv  14263  digit2  14387  nfile  14510  hashdifpr  14567  hashgt23el  14576  hashreshashfun  14591  hashf1dmcdm  14596  hash3tpexb  14646  fi1uzind  14659  ccatval1  14729  ccatass  14741  swrdval  14799  swrdnd  14812  swrd0  14816  swrdfv2  14819  pfxsuff1eqwrdeq  14856  swrdswrdlem  14861  pfxccatin12lem2a  14884  pfxccatin12lem1  14885  repswccat  14945  cshwidxmod  14962  cshwidxmodr  14963  cshf1  14969  repswcshw  14971  2cshw  14972  2cshwcom  14975  2cshwcshw  14984  cshwcsh2id  14987  ccatco  14994  2swrd2eqwrdeq  15115  wwlktovf  15118  brcnvtrclfv  15165  shftval2  15237  mulre  15297  absdiv  15471  absdiflt  15494  absdifle  15495  abs3dif  15508  cau3  15532  ello12r  15693  elo12r  15704  modfsummods  15969  geoisum1c  16058  rpnnen2lem4  16394  rpnnen2lem7  16397  addmulmodb  16444  dvdsmulc  16462  dvdsmulcr  16464  dvdsmultr1  16475  dvdsmultr2  16477  dvdssub2  16480  oexpneg  16524  divalgb  16583  ndvdsadd  16589  sadass  16650  modgcd  16714  dvdsgcd  16726  dvdsgcdb  16727  gcdass  16729  mulgcd  16730  absmulgcd  16731  rpmulgcd  16740  expgcd  16746  zexpgcd  16748  nn0seqcvgd  16754  algcvga  16763  lcmdvdsb  16797  lcmass  16798  lcmfunsnlem1  16821  lcmfunsnlem2lem1  16822  lcmfunsnlem2lem2  16823  coprmdvds  16837  coprmdvds2  16838  rpmul  16843  cncongr1  16851  cncongr2  16852  qnumdenbi  16929  modprm0  16992  coprimeprodsq  16995  pythagtriplem4  17006  pythagtriplem8  17010  pythagtriplem9  17011  pythagtriplem12  17013  pythagtriplem14  17015  pythagtriplem16  17017  pcpremul  17030  pcgcd  17065  vdwapval  17160  vdwapun  17161  prmgaplem3  17240  prmgaplem4  17241  prmgaplem7  17244  prmgapprmolem  17248  mreiincl  17775  mreincl  17778  mremre  17783  mrcss  17799  catcisolem  18294  pleval2  18518  pospo  18526  latlem  18620  latjcom  18630  latmcom  18646  lubss  18696  lubun  18698  clatglbss  18702  ipole  18717  ipolt  18718  pslem  18755  dirtr  18785  gsumsgrpccat  19045  gsumws2  19047  frmdmnd  19064  symggrplem  19089  isgrpi  19179  grpsubrcan  19240  grpinvsub  19241  grpsubeq0  19245  grpsubadd0sub  19246  grpnpcan  19251  qussub  19415  ghmsub  19447  symgpssefmnd  19619  symggrp  19623  symgextsymg  19647  gsmsymgreqlem2  19654  symgfixfolem1  19661  pmtrprfv3  19677  symggen  19693  lsmass  19892  efgsrel  19957  cntzcmn  20063  dvrcl  20643  unitdvcl  20644  dvrcan1  20648  subrngmre  20823  subrgmre  20858  rhmsubclem2  20947  rrgeq0  20961  abvsubtri  21093  abvtrivd  21098  lmodvsubval2  21201  rmodislmodlem  21213  rmodislmod  21214  lss0cl  21231  lssintcl  21248  lssincl  21249  reslmhm2  21337  lspvadd  21380  lspsntrim  21382  islbs3  21442  unichnlidl  21525  rnglidlmmgm  21542  cncrng  21708  xrsmcmn  21710  cndrng  21716  cnsrng  21721  absabv  21739  xrs1mnd  21755  psgnco  21898  zrhpsgninv  21900  zrhpsgnevpm  21906  zrhpsgnodpm  21907  zrhpsgnelbas  21909  zrhcopsgnelbas  21910  uvcresum  22108  lindfmm  22142  lindsmm  22143  evlsval2  22405  mamudm  22719  mamufacex  22720  matsubgcell  22758  matsc  22774  scmatscmide  22831  scmatrhmcl  22852  1marepvsma1  22907  m1detdiag  22921  mdetralt  22932  m2detleiblem7  22951  gsummatr01lem3  22981  gsummatr01  22983  smadiadetlem0  22985  decpmate  23093  decpmatcl  23094  pm2mpcl  23124  pm2mpghmlem2  23139  chfacfscmul0  23185  chfacfscmulgsum  23187  chfacfpmmul0  23189  chfacfpmmulgsum  23191  unopn  23230  clsss  23381  cldmre  23405  toponmre  23420  opnssneib  23442  restabs  23492  restcls  23508  restntr  23509  hausnei2  23680  cmpsublem  23726  bwth  23737  hausmapdom  23828  ptpjcn  23939  upxp  23951  ptrescn  23967  xkopjcn  23984  fbssfi  24165  snfil  24192  ufprim  24237  rnelfm  24281  flimrest  24311  fclsrest  24352  tmdgsum  24423  blpnfctr  24764  mscl  24789  xmscl  24790  xmsge0  24791  xmseq0  24792  restmetu  24898  ngpds  24932  tngngp3  24984  unitnmn0  24996  xrsxmet  25138  metds0  25179  mpomulcn  25197  cncfmptc  25242  isclmp  25427  cnlmod  25470  ncvsi  25481  cphsqrtcl  25514  cfil3i  25599  cfilres  25626  cmssmscld  25680  cmmbl  25864  voliunlem2  25881  itg2ub  26063  itgrecl  26127  r1pid  26488  eflogeq  26939  cxpadd  27016  cxpcom  27076  logbchbase  27108  relogbreexp  27112  relogbzexp  27113  relogbmulexp  27115  logbleb  27120  logblt  27121  lawcos  27153  pythag  27154  asinsinb  27234  acoscosb  27235  atantanb  27261  amgmlem  27326  lgsneg  27657  lgsne0  27671  lgsmodeq  27678  lgsmulsqcoprm  27679  gausslemma2dlem1a  27701  2sqreulem2  27788  ltsres  28028  noetainflem1  28103  ltlestr  28126  lestr  28128  nocvxmin  28150  madebdaylemold  28293  lrrecpo  28336  ltadds2im  28381  leadds1im  28382  leadds2im  28383  leadds1  28384  leadds2  28385  ltadds1  28387  addscan2  28388  addscan1  28389  subadds  28465  ltsubs1  28471  divscl  28618  oncutlt  28659  zsoring  28804  expscllem  28825  brbtwn2  29492  colinearalg  29497  eleesubd  29499  axcgrrflx  29501  axcgrtr  29502  axsegcon  29514  ax5seglem1  29515  ax5seglem2  29516  ax5seglem4  29519  axbtwnid  29526  axlowdimlem14  29542  axlowdim  29548  axcontlem5  29555  axcontlem7  29557  nb3grprlem2  29971  cplgr3v  30025  cusgrsizeindslem  30041  sizusglecusglem2  30052  umgr2v2e  30115  cusgrrusgr  30171  iswlk  30200  edginwlk  30224  uspgr2wlkeq  30235  uspgr2wlkeq2  30236  uspgr2wlkeqi  30237  wlkonprop  30246  wlkon2n0  30254  subgrwlk  30278  pthdadjvtx  30322  upgr2pthnlp  30327  spthonepeq  30347  pthdlem2lem  30362  crctcshwlkn0lem3  30410  crctcshwlkn0lem5  30412  wlkiswwlks2lem4  30470  wlkiswwlks2lem6  30472  wlklnwwlkln2lem  30480  wwlksnred  30490  wwlksnextbi  30492  wwlksnextwrd  30495  2pthdlem1  30528  2wlkdlem10  30533  umgr2adedgwlkonALT  30545  elwwlks2s3  30549  elwwlks2ons3im  30552  s3wwlks2on  30554  sps3wwlks2on  30555  2wspdisj  30563  2wspiundisj  30564  clwwlkgt0  30586  clwlkclwwlklem2a4  30597  clwlkclwwlklem2a  30598  clwlkclwwlk  30602  clwlkclwwlk2  30603  clwlkclwwlkfo  30609  clwwisshclwwslemlem  30613  erclwwlktr  30622  clwwlkf  30647  wwlksubclwwlk  30658  erclwwlkntr  30671  clwwlknon  30690  frcond1  30876  frgr3v  30885  3vfriswmgr  30888  frgrwopreglem4a  30920  frrusgrord0lem  30949  clwwnonrepclwwnon  30955  extwwlkfab  30962  numclwwlk1lem2f1  30967  numclwwlk1lem2fo  30968  clwlknon2num  30978  numclwwlk2lem1  30986  numclwlk2lem2f  30987  numclwlk2lem2f1o  30989  numclwwlk2  30991  frgrreggt1  31003  friendshipgt3  31008  imsmetlem  31301  nmoxr  31377  nmoolb  31382  blometi  31414  phpar2  31434  phpar  31435  ipasslem5  31446  hvadd32  31645  hvaddsub12  31649  hvaddsubass  31652  hvsubass  31655  hvsub32  31656  hvsubdistr1  31660  hvsubdistr2  31661  hvmulcan  31683  hvmulcan2  31684  hvsubcan  31685  his5  31697  his2sub  31703  hhssabloilem  31872  hhssnv  31875  shlej2  31972  pjoi0  32328  hodcl  32358  hoadd32  32394  hosubdi  32419  hosubsub2  32423  hoaddsubass  32426  hosubsub4  32429  nmoplb  32518  unop  32526  hmop  32533  nmfnlb  32535  lnopmul  32578  kbass1  32727  kbass2  32728  leopmul2i  32746  leoptr  32748  cvntr  32903  mdslmd4i  32944  mdexchi  32946  atcv1  32991  sumdmdii  33026  fcoinvbr  33250  fpwrelmapffs  33376  xreceu  33538  isinftm  33792  inlidl  34021  unitdivcld  34583  esummulc1  34763  hasheuni  34767  unelsiga  34816  inelpisys  34837  carsgsigalem  34997  signswmnd  35236  bnj545  35575  bnj594  35592  bnj1311  35704  weexenwe  35816  fineqvac  35844  fineqvnttrclselem3  35851  fineqvinfep  35853  onprcf1acwevdlem1  35968  usgrgt2cycl  35989  acycgr1v  35994  cvmsf1o  36127  cvmscld  36128  satefvfmla1  36280  elnanelprv  36284  lediv2aALT  36532  gcd32  36610  dfrdg4  36811  brcolinear  36920  colinearex  36921  ltnmul  37061  ltnadd  37063  nn0prpwlem  37206  clsun  37212  fnemeet1  37250  fnemeet2  37251  fnejoin1  37252  fnejoin2  37253  eltail  37258  rdgeqoa  38402  nlpineqsn  38440  lindsadd  38645  poimirlem28  38675  cnambfre  38695  ftc1anclem4  38723  cocanfo  38762  f1ocan1fv  38769  metf1o  38798  ismtybnd  38850  ghomco  38934  isdrngo2  39001  inidl  39073  igenmin  39107  brxrn  39424  brredunds  39751  cmtvalN  40377  cvrval  40435  pmapmeet  40939  paddval  40964  paddssat  40980  elpcliN  41059  pclssN  41060  pclunN  41064  paddunN  41093  poldmj1N  41094  tendoplcl2  41944  tendoplcl  41947  dihmeet  42509  lcmineqlem1  43188  reltsub1  43546  reltsubadd2  43547  resubsub4  43549  reppncan  43553  resubdi  43556  readdcan2  43573  subresre  43591  mapco2g  43834  mzpcompact2lem  43871  eqrabdioph  43897  lerabdioph  43921  eluzrabdioph  43922  ltrabdioph  43924  nerabdioph  43925  dvdsrabdioph  43926  reglogcl  44006  rmxyadd  44037  rmyabs  44074  congadd  44082  congabseq  44090  rmydioph  44130  mendring  44299  mendlmod  44300  iocinico  44323  omge1  44408  relexp0a  44825  relexpaddss  44827  brcoffn  45139  ismnushort  45394  dvconstbi  45427  uzwo4  46178  ssin0  46180  ssinc  46210  ssdec  46211  fvmpt2bd  46293  disjf1o  46314  ssnnf1octb  46317  sub31  46414  fperiodmullem  46427  ssfiunibd  46433  infxr  46486  fmul01  46700  islptre  46739  lptre2pt  46758  limcleqr  46762  limclner  46769  limsuppnflem  46828  limsupvaluz2  46856  supcnvlimsup  46858  xlimmnfvlem2  46951  xlimmnfv  46952  xlimpnfvlem2  46955  xlimpnfv  46956  climxlim2lem  46963  coskpi2  46984  cosknegpi  46987  dvnmptdivc  47056  dvdsn1add  47057  dvnmptconst  47059  dvmptfprod  47063  dvnprodlem1  47064  dvnprodlem2  47065  ovolsplit  47106  stoweidlem60  47178  stowei  47182  dirkeritg  47220  fourierdlem70  47294  fourierdlem71  47295  fourierdlem103  47327  fourierdlem104  47328  fouriersw  47349  rrxtopnfi  47405  saluncl  47435  salexct  47452  sge0ltfirp  47518  sge0iunmpt  47536  meadjiunlem  47583  meaiuninc3v  47602  carageniuncllem1  47639  caratheodorylem1  47644  ovncvrrp  47682  ovnsubaddlem1  47688  hspmbllem2  47745  ovolval5lem3  47772  smfpimbor1lem1  47916  smfsuplem1  47929  smflimsuplem4  47941  sigarls  47975  cnambpcma  48472  elfzelfzlble  48499  submodaddmod  48525  difltmodne  48526  m1mod0mod1  48538  modmkpkne  48545  mod2addne  48548  modm2nep1  48550  modm1nep2  48552  modm1nem2  48553  fsumsplitsndif  48559  fundcmpsurinjALT  48602  iccpartiltu  48612  prproropf1olem2  48694  fmtno4prmfac  48765  2pwp1prmfmtno  48783  lighneallem4b  48802  nprmdvdsfacm1lem4  48816  mogoldbblem  48926  gbegt5  48967  sbgoldbm  48990  nnsum3primesle9  49000  nnsum4primesodd  49002  nnsum4primesoddALTV  49003  evengpoap3  49005  nnsum4primesevenALTV  49007  clnbgredg  49046  opstrgric  49132  clnbgrgrimlem  49139  grtrif1o  49148  isubgr3stgrlem1  49172  isubgr3stgrlem4  49175  gpgusgralem  49262  gpg3nbgrvtx0  49282  isupwlk  49342  lidldomnnring  49441  2zrngacmnd  49453  rhmsubcALTVlem2  49487  fprmappr  49565  zlmodzxzscm  49577  gsumlsscl  49600  lincvalsng  49636  lincvalpr  49638  lincdifsn  49644  linc1  49645  lincellss  49646  fdivmpt  49760  digexp  49827  2arymaptfo  49874  line  49953  rrxline  49955  itsclc0xyqsolr  49989  iscnrm3r  50170  resipos  50197  amgmwlem  51170