Theorem 3adant1 1123

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

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

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 1082

This theorem is referenced by:  3ad2ant2  1127  3ad2ant3  1128  3simpc  1143  eupickb  2692  spc3egv  3548  sbciegft  3742  reuhyp  5219  funopg  6266  funprg  6285  funtpg  6286  funcnvtp  6294  fvun1  6628  fnreseql  6690  xpprsng  6772  ftpg  6788  f13dfv  6903  mpoeq3ia  7097  ordunel  7405  fex2  7501  funexw  7516  poxp  7682  suppval1  7694  wfr3g  7811  smores3  7849  oaord  8030  oacan  8031  oaword  8032  omord  8051  omcan  8052  omwordri  8055  odi  8062  omass  8063  oeord  8071  oecan  8072  oewordri  8075  oeordsuc  8077  nnaord  8102  nnaordr  8103  nndi  8106  nnmass  8107  nnaword  8110  nnmord  8115  nnmwordri  8119  erov  8251  ecopovtrn  8257  ixpf  8339  mapxpen  8537  fimax2g  8617  unbnn  8627  funisfsupp  8691  inelfi  8735  elfiun  8747  sup0  8783  suppr  8788  infpr  8820  r111  9057  dif1card  9289  ackbij1lem16  9510  cff1  9533  cfflb  9534  cfsmolem  9545  fin23lem34  9621  hsmexlem2  9702  axcc3  9713  domtriomlem  9717  axdc3lem4  9728  axdc4lem  9730  axcclem  9732  konigthlem  9843  gchdomtri  9904  tskpr  10045  tskop  10046  tskuni  10058  tskun  10061  gruop  10080  gruun  10081  grudomon  10092  adderpqlem  10229  mulerpqlem  10230  addassnq  10233  mulassnq  10234  distrnq  10236  ltsonq  10244  ltanq  10246  ltmnq  10247  genpass  10284  distrlem1pr  10300  distrlem4pr  10301  ltsopr  10307  adddir  10485  axlttrn  10566  ltletr  10585  letr  10587  mul32  10659  mul31  10660  add32  10711  subsub23  10744  addsubass  10750  subcan2  10765  subsub2  10768  nppcan2  10771  sub32  10774  nnncan  10775  nnncan2  10777  pnpcan2  10780  subdi  10927  subdir  10928  receu  11139  mulcan1g  11147  mulcan2g  11148  divmul3  11157  divrec  11168  divrec2  11169  divsubdir  11188  subdivcomb2  11190  divdiv1  11205  redivcl  11213  div2neg  11217  ltmul2  11345  lemul1  11346  lemul2  11347  lemul2a  11349  lediv1  11359  gt0div  11360  ge0div  11361  mulsuble0b  11366  ltdivmul  11369  ledivmul  11370  ltdivmul2  11371  ledivmul2  11373  lemuldiv  11374  ltdiv23  11385  lediv23  11386  ledivp1i  11419  ltdivp1i  11420  uzind2  11929  nn0ind  11931  fnn0ind  11935  uz3m2nn  12144  xrltletr  12404  xrletr  12405  xrre2  12417  xrltmin  12429  xrlemin  12431  xleadd2a  12501  xleadd1  12502  xltadd2  12504  xmulasslem3  12533  xmulass  12534  xltmul2  12540  ixxdisj  12607  iooneg  12711  iccneg  12712  icoshft  12713  icoshftf1o  12714  icodisj  12716  snunioo  12718  fzen  12778  ssfzunsnext  12806  fzrev3  12827  2ffzeq  12882  fzoaddel2  12947  elfzodifsumelfzo  12957  ssfzoulel  12985  ssfzo12bi  12986  fzoshftral  13008  adddivflid  13042  flltdivnn0lt  13057  ltdifltdiv  13058  fldiv4p1lem1div2  13059  modcyc  13128  modcyc2  13129  modaddabs  13131  modsubmodmod  13152  modaddmodup  13156  modaddmulmod  13160  moddi  13161  modsubdir  13162  expdiv  13334  digit2  13451  nfile  13574  hashdifpr  13628  hashgt23el  13637  hashreshashfun  13652  fi1uzind  13705  ccatass  13790  lswccatn0lsw  13793  swrdval  13845  swrdnd  13856  swrd0  13860  swrdfv2  13863  pfxsuff1eqwrdeq  13901  ccatpfx  13903  swrdswrdlem  13906  pfxccatin12lem2a  13929  pfxccatin12lem1  13930  repswccat  13988  cshwidxmod  14005  cshwidxmodr  14006  cshf1  14012  repswcshw  14014  2cshw  14015  2cshwcom  14018  2cshwcshw  14027  cshwcsh2id  14030  ccatco  14037  pfx2  14149  2swrd2eqwrdeq  14155  wwlktovf  14158  brcnvtrclfv  14201  shftval2  14272  mulre  14318  absdiv  14493  absdiflt  14515  absdifle  14516  abs3dif  14529  cau3  14553  ello12r  14712  elo12r  14723  modfsummods  14985  geoisum1c  15073  rpnnen2lem4  15407  rpnnen2lem7  15410  dvdsmulc  15474  dvdsmulcr  15476  dvdsmultr1  15484  dvdsmultr2  15486  dvdssub2  15488  oexpneg  15531  divalgb  15592  ndvdsadd  15598  sadass  15657  modgcd  15717  dvdsgcd  15725  dvdsgcdb  15726  gcdass  15728  mulgcd  15729  absmulgcd  15730  rpmulgcd  15739  nn0seqcvgd  15747  algcvga  15756  lcmdvdsb  15790  lcmass  15791  lcmfunsnlem1  15814  lcmfunsnlem2lem1  15815  lcmfunsnlem2lem2  15816  coprmdvds  15830  coprmdvds2  15831  rpmul  15836  cncongr1  15844  cncongr2  15845  qnumdenbi  15917  modprm0  15975  coprimeprodsq  15978  pythagtriplem4  15989  pythagtriplem8  15993  pythagtriplem9  15994  pythagtriplem12  15996  pythagtriplem14  15998  pythagtriplem16  16000  pcpremul  16013  pcgcd  16047  vdwapval  16142  vdwapun  16143  prmgaplem3  16222  prmgaplem4  16223  prmgaplem7  16226  prmgapprmolem  16230  mreiincl  16700  mreincl  16703  mremre  16708  mrcss  16720  catcisolem  17199  pleval2  17408  pospo  17416  latlem  17492  latjcom  17502  latmcom  17518  lubss  17564  lubun  17566  clatglbss  17570  ipole  17601  ipolt  17602  pslem  17649  dirtr  17679  gsumws2  17822  frmdmnd  17839  isgrpi  17888  grpsubrcan  17941  grpinvsub  17942  grpsubeq0  17946  grpsubadd0sub  17947  grpnpcan  17952  qussub  18097  ghmsub  18111  symggrp  18263  symgextsymg  18287  gsmsymgreqlem2  18294  symgfixfolem1  18301  pmtrprfv3  18317  symggen  18333  lsmass  18527  efgsrel  18591  cntzcmn  18689  dvrcl  19130  unitdvcl  19131  dvrcan1  19135  subrgmre  19253  abvsubtri  19300  abvtrivd  19305  lmodvsubval2  19383  rmodislmodlem  19395  rmodislmod  19396  lss0cl  19412  lssintcl  19430  lssincl  19431  reslmhm2  19519  lspvadd  19562  lspsntrim  19564  islbs3  19621  rrgeq0  19756  evlsval2  19991  cncrng  20252  xrsmcmn  20254  cndrng  20260  cnsrng  20265  xrs1mnd  20269  absabv  20288  psgnco  20413  zrhpsgninv  20415  zrhpsgnevpm  20421  zrhpsgnodpm  20422  zrhpsgnelbas  20424  zrhcopsgnelbas  20425  uvcresum  20623  lindfmm  20657  lindsmm  20658  mamudm  20685  mamufacex  20686  matsubgcell  20731  matsc  20747  scmatscmide  20804  scmatrhmcl  20825  1marepvsma1  20880  m1detdiag  20894  mdetralt  20905  m2detleiblem7  20924  gsummatr01lem3  20954  gsummatr01  20956  smadiadetlem0  20958  decpmate  21062  decpmatcl  21063  pm2mpcl  21093  pm2mpghmlem2  21108  chfacfscmul0  21154  chfacfscmulgsum  21156  chfacfpmmul0  21158  chfacfpmmulgsum  21160  unopn  21199  clsss  21350  cldmre  21374  toponmre  21389  opnssneib  21411  restabs  21461  restcls  21477  restntr  21478  hausnei2  21649  cmpsublem  21695  bwth  21706  hausmapdom  21796  ptpjcn  21907  upxp  21919  ptrescn  21935  xkopjcn  21952  fbssfi  22133  snfil  22160  ufprim  22205  rnelfm  22249  flimrest  22279  fclsrest  22320  tmdgsum  22391  blpnfctr  22733  mscl  22758  xmscl  22759  xmsge0  22760  xmseq0  22761  restmetu  22867  ngpds  22900  tngngp3  22952  unitnmn0  22964  xrsxmet  23104  metds0  23145  cncfmptc  23206  isclmp  23388  cnlmod  23431  ncvsi  23442  cphsqrtcl  23475  cfil3i  23559  cfilres  23586  cmssmscld  23640  cmmbl  23822  voliunlem2  23839  itg2ub  24021  itgrecl  24085  tdeglem3  24340  r1pid  24440  eflogeq  24870  cxpadd  24947  cxpcom  25005  logbchbase  25034  relogbreexp  25038  relogbzexp  25039  relogbmulexp  25041  logbleb  25046  logblt  25047  lawcos  25079  pythag  25080  asinsinb  25160  acoscosb  25161  atantanb  25187  amgmlem  25253  lgsneg  25583  lgsne0  25597  lgsmodeq  25604  lgsmulsqcoprm  25605  gausslemma2dlem1a  25627  2sqreulem2  25714  brbtwn2  26378  colinearalg  26383  eleesubd  26385  axcgrrflx  26387  axcgrtr  26388  axsegcon  26400  ax5seglem1  26401  ax5seglem2  26402  ax5seglem4  26405  axbtwnid  26412  axlowdimlem14  26428  axlowdim  26434  axcontlem5  26441  axcontlem7  26443  nb3grprlem2  26850  cplgr3v  26904  cusgrsizeindslem  26920  sizusglecusglem2  26931  umgr2v2e  26994  cusgrrusgr  27050  iswlk  27079  edginwlk  27103  uspgr2wlkeq  27114  uspgr2wlkeq2  27115  uspgr2wlkeqi  27116  wlkonprop  27126  wlkon2n0  27134  pthdadjvtx  27197  upgr2pthnlp  27199  spthonepeq  27219  pthdlem2lem  27234  crctcshwlkn0lem3  27276  crctcshwlkn0lem5  27278  wlkiswwlks2lem4  27336  wlkiswwlks2lem6  27338  wlklnwwlkln2lem  27346  wwlksnred  27356  wwlksnextbi  27358  wwlksnextwrd  27361  2pthdlem1  27395  2wlkdlem10  27400  umgr2adedgwlkonALT  27412  elwwlks2s3  27416  elwwlks2ons3im  27419  s3wwlks2on  27421  2wspdisj  27427  2wspiundisj  27428  clwwlkgt0  27450  clwlkclwwlklem2a4  27461  clwlkclwwlklem2a  27462  clwlkclwwlk  27466  clwlkclwwlk2  27467  clwlkclwwlkfo  27473  clwwisshclwwslemlem  27477  erclwwlktr  27486  clwwlkf  27512  wwlksubclwwlk  27523  erclwwlkntr  27536  clwwlknon  27555  frcond1  27733  frgr3v  27742  3vfriswmgr  27745  frgrwopreglem4a  27777  frrusgrord0lem  27806  clwwnonrepclwwnon  27812  extwwlkfab  27819  numclwwlk1lem2f1  27824  numclwwlk1lem2fo  27825  clwlknon2num  27835  numclwwlk2lem1  27843  numclwlk2lem2f  27844  numclwlk2lem2f1o  27846  numclwwlk2  27848  frgrreggt1  27860  friendshipgt3  27865  imsmetlem  28154  nmoxr  28230  nmoolb  28235  blometi  28267  phpar2  28287  phpar  28288  ipasslem5  28299  hvadd32  28498  hvaddsub12  28502  hvaddsubass  28505  hvsubass  28508  hvsub32  28509  hvsubdistr1  28513  hvsubdistr2  28514  hvmulcan  28536  hvmulcan2  28537  hvsubcan  28538  his5  28550  his2sub  28556  hhssabloilem  28725  hhssnv  28728  shlej2  28825  pjoi0  29181  hodcl  29211  hoadd32  29247  hosubdi  29272  hosubsub2  29276  hoaddsubass  29279  hosubsub4  29282  nmoplb  29371  unop  29379  hmop  29386  nmfnlb  29388  lnopmul  29431  kbass1  29580  kbass2  29581  leopmul2i  29599  leoptr  29601  cvntr  29756  mdslmd4i  29797  mdexchi  29799  atcv1  29844  sumdmdii  29879  fcoinvbr  30044  fpwrelmapffs  30154  xreceu  30278  isinftm  30444  unitdivcld  30757  esummulc1  30953  hasheuni  30957  unelsiga  31006  inelpisys  31026  carsgsigalem  31186  signswmnd  31440  bnj545  31779  bnj594  31796  bnj1311  31906  hashf1dmcdm  31966  usgrgt2cycl  31987  subgrwlk  31989  acycgr1v  32006  cvmsf1o  32129  cvmscld  32130  satefvfmla1  32282  elnanelprv  32286  lediv2aALT  32530  gcd32  32593  fununiq  32622  trpredpo  32685  poseq  32706  frr3g  32732  sltres  32780  sltletr  32846  sletr  32848  nocvxmin  32859  dfrdg4  33023  brcolinear  33131  colinearex  33132  nn0prpwlem  33281  clsun  33287  fnemeet1  33325  fnemeet2  33326  fnejoin1  33327  fnejoin2  33328  eltail  33333  rdgeqoa  34203  nlpineqsn  34241  curf  34422  lindsadd  34437  poimirlem28  34472  cnambfre  34492  ftc1anclem4  34522  cocanfo  34546  f1ocan1fv  34554  metf1o  34583  ismtybnd  34638  ghomco  34722  isdrngo2  34789  inidl  34861  igenmin  34895  brxrn  35178  brredunds  35413  cmtvalN  35899  cvrval  35957  pmapmeet  36461  paddval  36486  paddssat  36502  elpcliN  36581  pclssN  36582  pclunN  36586  paddunN  36615  poldmj1N  36616  tendoplcl2  37466  tendoplcl  37469  dihmeet  38031  expgcd  38726  zexpgcd  38728  resubsub4  38761  reppncan  38765  resubdi  38768  mapco2g  38817  mzpcompact2lem  38854  eqrabdioph  38880  lerabdioph  38908  eluzrabdioph  38909  ltrabdioph  38911  nerabdioph  38912  dvdsrabdioph  38913  reglogcl  38993  rmxyadd  39024  rmyabs  39061  congadd  39069  congabseq  39077  rmydioph  39117  mendring  39298  mendlmod  39299  iocinico  39324  relexp0a  39567  relexpaddss  39569  brcoffn  39886  dvconstbi  40225  uzwo4  40875  ssin0  40877  ssinc  40913  ssdec  40914  unima  40983  fvmpt2bd  40987  disjf1o  41013  ssnnf1octb  41017  sub31  41119  fperiodmullem  41132  ssfiunibd  41138  infxr  41197  fmul01  41424  islptre  41463  lptre2pt  41484  limcleqr  41488  limclner  41495  limsuppnflem  41554  limsupvaluz2  41582  supcnvlimsup  41584  xlimmnfvlem2  41677  xlimmnfv  41678  xlimpnfvlem2  41681  xlimpnfv  41682  climxlim2lem  41689  coskpi2  41710  cosknegpi  41713  dvnmptdivc  41786  dvdsn1add  41787  dvnmptconst  41789  dvmptfprod  41793  dvnprodlem1  41794  dvnprodlem2  41795  ovolsplit  41837  stoweidlem60  41909  stowei  41913  dirkeritg  41951  fourierdlem70  42025  fourierdlem71  42026  fourierdlem103  42058  fourierdlem104  42059  fouriersw  42080  rrxtopnfi  42136  saluncl  42166  salexct  42181  sge0ltfirp  42246  sge0iunmpt  42264  meadjiunlem  42311  meaiuninc3v  42330  carageniuncllem1  42367  caratheodorylem1  42372  ovncvrrp  42410  ovnsubaddlem1  42416  hspmbllem2  42473  ovolval5lem3  42500  smfpimbor1lem1  42637  smfsuplem1  42649  smflimsuplem4  42661  sigarls  42678  cnambpcma  43032  elfzelfzlble  43059  fzoopth  43065  m1mod0mod1  43067  fsumsplitsndif  43071  iccpartiltu  43086  prproropf1olem2  43170  fmtno4prmfac  43238  2pwp1prmfmtno  43256  lighneallem4b  43278  mogoldbblem  43389  gbegt5  43430  sbgoldbm  43453  nnsum3primesle9  43463  nnsum4primesodd  43465  nnsum4primesoddALTV  43466  evengpoap3  43468  nnsum4primesevenALTV  43470  isomgrtr  43508  strisomgrop  43509  isupwlk  43515  lidldomnnring  43701  2zrngacmnd  43713  rhmsubclem2  43858  rhmsubcALTVlem2  43876  zlmodzxzscm  43905  gsumlsscl  43933  lincvalsng  43973  lincvalpr  43975  lincdifsn  43981  linc1  43982  lincellss  43983  difmodm1lt  44085  fdivmpt  44103  digexp  44170  line  44222  rrxline  44224  itsclc0xyqsolr  44259  amgmwlem  44405