Theorem 3adant1 1131

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

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

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 1089

This theorem is referenced by:  3ad2ant2  1135  3ad2ant3  1136  3simpc  1151  eupickb  2636  spc3egv  3559  sbciegftOLD  3780  reuhyp  5367  predtrss  6288  onunel  6432  funopg  6534  funprg  6554  funtpg  6555  funcnvtp  6563  unima  6917  fvun1  6933  fnreseql  7002  xpprsng  7095  ftpg  7111  f1ounsn  7228  f13dfv  7230  f1ocoima  7259  f1ofvswap  7262  mpoeq3ia  7446  ordunel  7779  fex2  7888  funexw  7906  poxp  8080  poxp2  8095  poxp3  8102  poseq  8110  suppval1  8118  wfr3g  8271  smores3  8295  oaord  8484  oacan  8485  oaword  8486  omord  8505  omcan  8506  omwordri  8509  odi  8516  omass  8517  oeord  8526  oecan  8527  oewordri  8530  oeordsuc  8532  nnaord  8557  nnaordr  8558  nndi  8561  nnmass  8562  nnaword  8565  nnmord  8570  nnmwordri  8574  naddelim  8624  naddel1  8625  naddel2  8626  naddss1  8627  naddss2  8628  naddasslem2  8633  nadd32  8635  erov  8763  ecopovtrn  8769  ixpf  8870  f1oen4g  8913  f1dom4g  8914  mapxpen  9083  ssfi  9109  sbthfilem  9134  sbthfi  9135  onomeneq  9150  fimax2g  9198  unbnn  9208  funisfsupp  9282  inelfi  9333  elfiun  9345  sup0  9382  suppr  9387  infpr  9420  ttrclss  9641  frr3g  9680  r111  9699  dif1card  9932  ackbij1lem16  10156  cff1  10180  cfflb  10181  cfsmolem  10192  fin23lem34  10268  hsmexlem2  10349  axcc3  10360  domtriomlem  10364  axdc3lem4  10375  axdc4lem  10377  axcclem  10379  konigthlem  10491  gchdomtri  10552  tskpr  10693  tskop  10694  tskuni  10706  tskun  10709  gruop  10728  gruun  10729  grudomon  10740  adderpqlem  10877  mulerpqlem  10878  addassnq  10881  mulassnq  10882  distrnq  10884  ltsonq  10892  ltanq  10894  ltmnq  10895  genpass  10932  distrlem1pr  10948  distrlem4pr  10949  ltsopr  10955  adddir  11135  axlttrn  11217  ltletr  11237  letr  11239  mul32  11311  mul31  11312  add32  11364  subsub23  11397  addsubass  11402  subcan2  11418  subsub2  11421  nppcan2  11424  sub32  11427  nnncan  11428  nnncan2  11430  pnpcan2  11433  subdi  11582  subdir  11583  receu  11794  mulcan1g  11802  mulcan2g  11803  divmul3  11813  divrec  11824  divrec2  11825  div11  11836  divsubdir  11847  subdivcomb2  11849  divdiv1  11864  redivcl  11872  div2neg  11876  ltmul2  12004  lemul1  12005  lemul2  12006  lemul2a  12008  lediv1  12019  gt0div  12020  ge0div  12021  mulsuble0b  12026  ltdivmul  12029  ledivmul  12030  ltdivmul2  12031  ledivmul2  12033  lemuldiv  12034  ltdiv23  12045  lediv23  12046  ledivp1i  12079  ltdivp1i  12080  uzind2  12597  nn0ind  12599  fnn0ind  12603  uz3m2nn  12819  xrltletr  13083  xrletr  13084  xrre2  13097  xrltmin  13109  xrlemin  13111  xleadd2a  13181  xleadd1  13182  xltadd2  13184  xmulasslem3  13213  xmulass  13214  xltmul2  13220  ixxdisj  13288  iooneg  13399  iccneg  13400  icoshft  13401  icoshftf1o  13402  icodisj  13404  snunioo  13406  fzen  13469  ssfzunsnext  13497  fzrev3  13518  2ffzeq  13577  fzoaddel2  13648  elfzodifsumelfzo  13659  ssfzoulel  13688  ssfzo12bi  13689  fzoopth  13690  fzoshftral  13715  adddivflid  13750  flltdivnn0lt  13765  ltdifltdiv  13766  fldiv4p1lem1div2  13767  modcyc  13838  modcyc2  13839  modaddabs  13843  muladdmod  13847  modsubmodmod  13865  modaddmodup  13869  modaddmulmod  13873  moddi  13874  modsubdir  13875  expdiv  14048  digit2  14171  nfile  14294  hashdifpr  14350  hashgt23el  14359  hashreshashfun  14374  hashf1dmcdm  14379  hash3tpexb  14429  fi1uzind  14442  ccatval1  14512  ccatass  14524  swrdval  14579  swrdnd  14590  swrd0  14594  swrdfv2  14597  pfxsuff1eqwrdeq  14634  swrdswrdlem  14639  pfxccatin12lem2a  14662  pfxccatin12lem1  14663  repswccat  14721  cshwidxmod  14738  cshwidxmodr  14739  cshf1  14745  repswcshw  14747  2cshw  14748  2cshwcom  14751  2cshwcshw  14760  cshwcsh2id  14763  ccatco  14770  2swrd2eqwrdeq  14888  wwlktovf  14891  brcnvtrclfv  14938  shftval2  15010  mulre  15056  absdiv  15230  absdiflt  15253  absdifle  15254  abs3dif  15267  cau3  15291  ello12r  15452  elo12r  15463  modfsummods  15728  geoisum1c  15815  rpnnen2lem4  16154  rpnnen2lem7  16157  addmulmodb  16204  dvdsmulc  16222  dvdsmulcr  16224  dvdsmultr1  16235  dvdsmultr2  16237  dvdssub2  16240  oexpneg  16284  divalgb  16343  ndvdsadd  16349  sadass  16410  modgcd  16471  dvdsgcd  16483  dvdsgcdb  16484  gcdass  16486  mulgcd  16487  absmulgcd  16488  rpmulgcd  16496  expgcd  16502  zexpgcd  16504  nn0seqcvgd  16509  algcvga  16518  lcmdvdsb  16552  lcmass  16553  lcmfunsnlem1  16576  lcmfunsnlem2lem1  16577  lcmfunsnlem2lem2  16578  coprmdvds  16592  coprmdvds2  16593  rpmul  16598  cncongr1  16606  cncongr2  16607  qnumdenbi  16683  modprm0  16745  coprimeprodsq  16748  pythagtriplem4  16759  pythagtriplem8  16763  pythagtriplem9  16764  pythagtriplem12  16766  pythagtriplem14  16768  pythagtriplem16  16770  pcpremul  16783  pcgcd  16818  vdwapval  16913  vdwapun  16914  prmgaplem3  16993  prmgaplem4  16994  prmgaplem7  16997  prmgapprmolem  17001  mreiincl  17527  mreincl  17530  mremre  17535  mrcss  17551  catcisolem  18046  pleval2  18270  pospo  18278  latlem  18372  latjcom  18382  latmcom  18398  lubss  18448  lubun  18450  clatglbss  18454  ipole  18469  ipolt  18470  pslem  18507  dirtr  18537  gsumsgrpccat  18777  gsumws2  18779  frmdmnd  18796  symggrplem  18821  isgrpi  18901  grpsubrcan  18963  grpinvsub  18964  grpsubeq0  18968  grpsubadd0sub  18969  grpnpcan  18974  qussub  19132  ghmsub  19165  symgpssefmnd  19337  symggrp  19341  symgextsymg  19365  gsmsymgreqlem2  19372  symgfixfolem1  19379  pmtrprfv3  19395  symggen  19411  lsmass  19610  efgsrel  19675  cntzcmn  19781  dvrcl  20352  unitdvcl  20353  dvrcan1  20357  subrngmre  20507  subrgmre  20542  rhmsubclem2  20631  rrgeq0  20645  abvsubtri  20772  abvtrivd  20777  lmodvsubval2  20880  rmodislmodlem  20892  rmodislmod  20893  lss0cl  20910  lssintcl  20927  lssincl  20928  reslmhm2  21017  lspvadd  21060  lspsntrim  21062  islbs3  21122  rnglidlmmgm  21212  cncrng  21355  cncrngOLD  21356  xrsmcmn  21358  cndrng  21365  cndrngOLD  21366  cnsrng  21372  absabv  21391  xrs1mnd  21407  psgnco  21550  zrhpsgninv  21552  zrhpsgnevpm  21558  zrhpsgnodpm  21559  zrhpsgnelbas  21561  zrhcopsgnelbas  21562  uvcresum  21760  lindfmm  21794  lindsmm  21795  evlsval2  22054  mamudm  22351  mamufacex  22352  matsubgcell  22390  matsc  22406  scmatscmide  22463  scmatrhmcl  22484  1marepvsma1  22539  m1detdiag  22553  mdetralt  22564  m2detleiblem7  22583  gsummatr01lem3  22613  gsummatr01  22615  smadiadetlem0  22617  decpmate  22722  decpmatcl  22723  pm2mpcl  22753  pm2mpghmlem2  22768  chfacfscmul0  22814  chfacfscmulgsum  22816  chfacfpmmul0  22818  chfacfpmmulgsum  22820  unopn  22859  clsss  23010  cldmre  23034  toponmre  23049  opnssneib  23071  restabs  23121  restcls  23137  restntr  23138  hausnei2  23309  cmpsublem  23355  bwth  23366  hausmapdom  23456  ptpjcn  23567  upxp  23579  ptrescn  23595  xkopjcn  23612  fbssfi  23793  snfil  23820  ufprim  23865  rnelfm  23909  flimrest  23939  fclsrest  23980  tmdgsum  24051  blpnfctr  24392  mscl  24417  xmscl  24418  xmsge0  24419  xmseq0  24420  restmetu  24526  ngpds  24560  tngngp3  24612  unitnmn0  24624  xrsxmet  24766  metds0  24807  mpomulcn  24826  cncfmptc  24873  isclmp  25065  cnlmod  25108  ncvsi  25119  cphsqrtcl  25152  cfil3i  25237  cfilres  25264  cmssmscld  25318  cmmbl  25503  voliunlem2  25520  itg2ub  25702  itgrecl  25767  r1pid  26134  eflogeq  26579  cxpadd  26656  cxpcom  26716  logbchbase  26749  relogbreexp  26753  relogbzexp  26754  relogbmulexp  26756  logbleb  26761  logblt  26762  lawcos  26794  pythag  26795  asinsinb  26875  acoscosb  26876  atantanb  26902  amgmlem  26968  lgsneg  27300  lgsne0  27314  lgsmodeq  27321  lgsmulsqcoprm  27322  gausslemma2dlem1a  27344  2sqreulem2  27431  ltsres  27642  noetainflem1  27717  ltlestr  27740  lestr  27742  nocvxmin  27763  madebdaylemold  27906  lrrecpo  27949  ltadds2im  27994  leadds1im  27995  leadds2im  27996  leadds1  27997  leadds2  27998  ltadds1  28000  addscan2  28001  addscan1  28002  subadds  28078  ltsubs1  28084  divscl  28231  oncutlt  28272  zsoring  28417  expscllem  28438  brbtwn2  28990  colinearalg  28995  eleesubd  28997  axcgrrflx  28999  axcgrtr  29000  axsegcon  29012  ax5seglem1  29013  ax5seglem2  29014  ax5seglem4  29017  axbtwnid  29024  axlowdimlem14  29040  axlowdim  29046  axcontlem5  29053  axcontlem7  29055  nb3grprlem2  29466  cplgr3v  29520  cusgrsizeindslem  29537  sizusglecusglem2  29548  umgr2v2e  29611  cusgrrusgr  29667  iswlk  29696  edginwlk  29720  uspgr2wlkeq  29731  uspgr2wlkeq2  29732  uspgr2wlkeqi  29733  wlkonprop  29742  wlkon2n0  29750  pthdadjvtx  29813  upgr2pthnlp  29817  spthonepeq  29837  pthdlem2lem  29852  crctcshwlkn0lem3  29897  crctcshwlkn0lem5  29899  wlkiswwlks2lem4  29957  wlkiswwlks2lem6  29959  wlklnwwlkln2lem  29967  wwlksnred  29977  wwlksnextbi  29979  wwlksnextwrd  29982  2pthdlem1  30015  2wlkdlem10  30020  umgr2adedgwlkonALT  30032  elwwlks2s3  30036  elwwlks2ons3im  30039  s3wwlks2on  30041  sps3wwlks2on  30042  2wspdisj  30050  2wspiundisj  30051  clwwlkgt0  30073  clwlkclwwlklem2a4  30084  clwlkclwwlklem2a  30085  clwlkclwwlk  30089  clwlkclwwlk2  30090  clwlkclwwlkfo  30096  clwwisshclwwslemlem  30100  erclwwlktr  30109  clwwlkf  30134  wwlksubclwwlk  30145  erclwwlkntr  30158  clwwlknon  30177  frcond1  30353  frgr3v  30362  3vfriswmgr  30365  frgrwopreglem4a  30397  frrusgrord0lem  30426  clwwnonrepclwwnon  30432  extwwlkfab  30439  numclwwlk1lem2f1  30444  numclwwlk1lem2fo  30445  clwlknon2num  30455  numclwwlk2lem1  30463  numclwlk2lem2f  30464  numclwlk2lem2f1o  30466  numclwwlk2  30468  frgrreggt1  30480  friendshipgt3  30485  imsmetlem  30777  nmoxr  30853  nmoolb  30858  blometi  30890  phpar2  30910  phpar  30911  ipasslem5  30922  hvadd32  31121  hvaddsub12  31125  hvaddsubass  31128  hvsubass  31131  hvsub32  31132  hvsubdistr1  31136  hvsubdistr2  31137  hvmulcan  31159  hvmulcan2  31160  hvsubcan  31161  his5  31173  his2sub  31179  hhssabloilem  31348  hhssnv  31351  shlej2  31448  pjoi0  31804  hodcl  31834  hoadd32  31870  hosubdi  31895  hosubsub2  31899  hoaddsubass  31902  hosubsub4  31905  nmoplb  31994  unop  32002  hmop  32009  nmfnlb  32011  lnopmul  32054  kbass1  32203  kbass2  32204  leopmul2i  32222  leoptr  32224  cvntr  32379  mdslmd4i  32420  mdexchi  32422  atcv1  32467  sumdmdii  32502  fcoinvbr  32691  fpwrelmapffs  32823  xreceu  33013  isinftm  33274  unitdivcld  34078  esummulc1  34258  hasheuni  34262  unelsiga  34311  inelpisys  34331  carsgsigalem  34492  signswmnd  34734  bnj545  35070  bnj594  35087  bnj1311  35199  fissorduni  35265  r1filimi  35278  fineqvac  35291  fineqvnttrclselem3  35298  fineqvinfep  35300  usgrgt2cycl  35343  subgrwlk  35345  acycgr1v  35362  cvmsf1o  35485  cvmscld  35486  satefvfmla1  35638  elnanelprv  35642  lediv2aALT  35890  gcd32  35962  fununiq  35982  dfrdg4  36164  brcolinear  36272  colinearex  36273  nn0prpwlem  36535  clsun  36541  fnemeet1  36579  fnemeet2  36580  fnejoin1  36581  fnejoin2  36582  eltail  36587  rdgeqoa  37622  nlpineqsn  37660  curf  37846  lindsadd  37861  poimirlem28  37896  cnambfre  37916  ftc1anclem4  37944  cocanfo  37967  f1ocan1fv  37974  metf1o  38003  ismtybnd  38055  ghomco  38139  isdrngo2  38206  inidl  38278  igenmin  38312  brxrn  38631  brredunds  38958  cmtvalN  39584  cvrval  39642  pmapmeet  40146  paddval  40171  paddssat  40187  elpcliN  40266  pclssN  40267  pclunN  40271  paddunN  40300  poldmj1N  40301  tendoplcl2  41151  tendoplcl  41154  dihmeet  41716  lcmineqlem1  42396  reltsub1  42753  reltsubadd2  42754  resubsub4  42756  reppncan  42760  resubdi  42763  readdcan2  42780  subresre  42798  mapco2g  43068  mzpcompact2lem  43105  eqrabdioph  43131  lerabdioph  43159  eluzrabdioph  43160  ltrabdioph  43162  nerabdioph  43163  dvdsrabdioph  43164  reglogcl  43244  rmxyadd  43275  rmyabs  43312  congadd  43320  congabseq  43328  rmydioph  43368  mendring  43542  mendlmod  43543  iocinico  43566  omge1  43651  relexp0a  44069  relexpaddss  44071  brcoffn  44383  ismnushort  44654  dvconstbi  44687  uzwo4  45410  ssin0  45412  ssinc  45443  ssdec  45444  fvmpt2bd  45526  disjf1o  45547  ssnnf1octb  45550  sub31  45649  fperiodmullem  45662  ssfiunibd  45668  infxr  45722  fmul01  45937  islptre  45976  lptre2pt  45995  limcleqr  45999  limclner  46006  limsuppnflem  46065  limsupvaluz2  46093  supcnvlimsup  46095  xlimmnfvlem2  46188  xlimmnfv  46189  xlimpnfvlem2  46192  xlimpnfv  46193  climxlim2lem  46200  coskpi2  46221  cosknegpi  46224  dvnmptdivc  46293  dvdsn1add  46294  dvnmptconst  46296  dvmptfprod  46300  dvnprodlem1  46301  dvnprodlem2  46302  ovolsplit  46343  stoweidlem60  46415  stowei  46419  dirkeritg  46457  fourierdlem70  46531  fourierdlem71  46532  fourierdlem103  46564  fourierdlem104  46565  fouriersw  46586  rrxtopnfi  46642  saluncl  46672  salexct  46689  sge0ltfirp  46755  sge0iunmpt  46773  meadjiunlem  46820  meaiuninc3v  46839  carageniuncllem1  46876  caratheodorylem1  46881  ovncvrrp  46919  ovnsubaddlem1  46925  hspmbllem2  46982  ovolval5lem3  47009  smfpimbor1lem1  47153  smfsuplem1  47166  smflimsuplem4  47178  sigarls  47212  cnambpcma  47651  elfzelfzlble  47678  submodaddmod  47698  difltmodne  47699  m1mod0mod1  47711  modmkpkne  47718  mod2addne  47721  modm2nep1  47723  modm1nep2  47725  modm1nem2  47726  fsumsplitsndif  47730  fundcmpsurinjALT  47769  iccpartiltu  47779  prproropf1olem2  47861  fmtno4prmfac  47929  2pwp1prmfmtno  47947  lighneallem4b  47966  mogoldbblem  48077  gbegt5  48118  sbgoldbm  48141  nnsum3primesle9  48151  nnsum4primesodd  48153  nnsum4primesoddALTV  48154  evengpoap3  48156  nnsum4primesevenALTV  48158  clnbgredg  48197  opstrgric  48283  clnbgrgrimlem  48290  grtrif1o  48299  isubgr3stgrlem1  48323  isubgr3stgrlem4  48326  gpgusgralem  48413  gpg3nbgrvtx0  48433  isupwlk  48493  lidldomnnring  48593  2zrngacmnd  48605  rhmsubcALTVlem2  48639  fprmappr  48702  zlmodzxzscm  48714  gsumlsscl  48737  lincvalsng  48773  lincvalpr  48775  lincdifsn  48781  linc1  48782  lincellss  48783  fdivmpt  48897  digexp  48964  2arymaptfo  49011  line  49089  rrxline  49091  itsclc0xyqsolr  49126  iscnrm3r  49304  resipos  49331  amgmwlem  50158