Theorem 3adant1 1126

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  3ad2ant2  1130  3ad2ant3  1131  3simpc  1146  eupickb  2716  spc3egv  3604  sbciegft  3808  reuhyp  5313  funopg  6384  funprg  6403  funtpg  6404  funcnvtp  6412  unima  6734  fvun1  6749  fnreseql  6813  xpprsng  6897  ftpg  6913  f13dfv  7025  mpoeq3ia  7226  ordunel  7536  fex2  7632  funexw  7647  poxp  7816  suppval1  7830  wfr3g  7947  smores3  7984  oaord  8167  oacan  8168  oaword  8169  omord  8188  omcan  8189  omwordri  8192  odi  8199  omass  8200  oeord  8208  oecan  8209  oewordri  8212  oeordsuc  8214  nnaord  8239  nnaordr  8240  nndi  8243  nnmass  8244  nnaword  8247  nnmord  8252  nnmwordri  8256  erov  8388  ecopovtrn  8394  ixpf  8478  mapxpen  8677  fimax2g  8758  unbnn  8768  funisfsupp  8832  inelfi  8876  elfiun  8888  sup0  8924  suppr  8929  infpr  8961  r111  9198  dif1card  9430  ackbij1lem16  9651  cff1  9674  cfflb  9675  cfsmolem  9686  fin23lem34  9762  hsmexlem2  9843  axcc3  9854  domtriomlem  9858  axdc3lem4  9869  axdc4lem  9871  axcclem  9873  konigthlem  9984  gchdomtri  10045  tskpr  10186  tskop  10187  tskuni  10199  tskun  10202  gruop  10221  gruun  10222  grudomon  10233  adderpqlem  10370  mulerpqlem  10371  addassnq  10374  mulassnq  10375  distrnq  10377  ltsonq  10385  ltanq  10387  ltmnq  10388  genpass  10425  distrlem1pr  10441  distrlem4pr  10442  ltsopr  10448  adddir  10626  axlttrn  10707  ltletr  10726  letr  10728  mul32  10800  mul31  10801  add32  10852  subsub23  10885  addsubass  10890  subcan2  10905  subsub2  10908  nppcan2  10911  sub32  10914  nnncan  10915  nnncan2  10917  pnpcan2  10920  subdi  11067  subdir  11068  receu  11279  mulcan1g  11287  mulcan2g  11288  divmul3  11297  divrec  11308  divrec2  11309  divsubdir  11328  subdivcomb2  11330  divdiv1  11345  redivcl  11353  div2neg  11357  ltmul2  11485  lemul1  11486  lemul2  11487  lemul2a  11489  lediv1  11499  gt0div  11500  ge0div  11501  mulsuble0b  11506  ltdivmul  11509  ledivmul  11510  ltdivmul2  11511  ledivmul2  11513  lemuldiv  11514  ltdiv23  11525  lediv23  11526  ledivp1i  11559  ltdivp1i  11560  uzind2  12069  nn0ind  12071  fnn0ind  12075  uz3m2nn  12285  xrltletr  12544  xrletr  12545  xrre2  12557  xrltmin  12569  xrlemin  12571  xleadd2a  12641  xleadd1  12642  xltadd2  12644  xmulasslem3  12673  xmulass  12674  xltmul2  12680  ixxdisj  12747  iooneg  12851  iccneg  12852  icoshft  12853  icoshftf1o  12854  icodisj  12856  snunioo  12858  fzen  12918  ssfzunsnext  12946  fzrev3  12967  2ffzeq  13022  fzoaddel2  13087  elfzodifsumelfzo  13097  ssfzoulel  13125  ssfzo12bi  13126  fzoshftral  13148  adddivflid  13182  flltdivnn0lt  13197  ltdifltdiv  13198  fldiv4p1lem1div2  13199  modcyc  13268  modcyc2  13269  modaddabs  13271  modsubmodmod  13292  modaddmodup  13296  modaddmulmod  13300  moddi  13301  modsubdir  13302  expdiv  13474  digit2  13591  nfile  13714  hashdifpr  13770  hashgt23el  13779  hashreshashfun  13794  fi1uzind  13849  ccatval1  13924  ccatass  13936  swrdval  13999  swrdnd  14010  swrd0  14014  swrdfv2  14017  pfxsuff1eqwrdeq  14055  swrdswrdlem  14060  pfxccatin12lem2a  14083  pfxccatin12lem1  14084  repswccat  14142  cshwidxmod  14159  cshwidxmodr  14160  cshf1  14166  repswcshw  14168  2cshw  14169  2cshwcom  14172  2cshwcshw  14181  cshwcsh2id  14184  ccatco  14191  2swrd2eqwrdeq  14309  wwlktovf  14314  brcnvtrclfv  14357  shftval2  14428  mulre  14474  absdiv  14649  absdiflt  14671  absdifle  14672  abs3dif  14685  cau3  14709  ello12r  14868  elo12r  14879  modfsummods  15142  geoisum1c  15230  rpnnen2lem4  15564  rpnnen2lem7  15567  dvdsmulc  15631  dvdsmulcr  15633  dvdsmultr1  15641  dvdsmultr2  15643  dvdssub2  15645  oexpneg  15688  divalgb  15749  ndvdsadd  15755  sadass  15814  modgcd  15874  dvdsgcd  15886  dvdsgcdb  15887  gcdass  15889  mulgcd  15890  absmulgcd  15891  rpmulgcd  15900  nn0seqcvgd  15908  algcvga  15917  lcmdvdsb  15951  lcmass  15952  lcmfunsnlem1  15975  lcmfunsnlem2lem1  15976  lcmfunsnlem2lem2  15977  coprmdvds  15991  coprmdvds2  15992  rpmul  15997  cncongr1  16005  cncongr2  16006  qnumdenbi  16078  modprm0  16136  coprimeprodsq  16139  pythagtriplem4  16150  pythagtriplem8  16154  pythagtriplem9  16155  pythagtriplem12  16157  pythagtriplem14  16159  pythagtriplem16  16161  pcpremul  16174  pcgcd  16208  vdwapval  16303  vdwapun  16304  prmgaplem3  16383  prmgaplem4  16384  prmgaplem7  16387  prmgapprmolem  16391  mreiincl  16861  mreincl  16864  mremre  16869  mrcss  16881  catcisolem  17360  pleval2  17569  pospo  17577  latlem  17653  latjcom  17663  latmcom  17679  lubss  17725  lubun  17727  clatglbss  17731  ipole  17762  ipolt  17763  pslem  17810  dirtr  17840  gsumsgrpccat  17998  gsumws2  18001  frmdmnd  18018  symggrplem  18043  isgrpi  18120  grpsubrcan  18174  grpinvsub  18175  grpsubeq0  18179  grpsubadd0sub  18180  grpnpcan  18185  qussub  18334  ghmsub  18360  symgpssefmnd  18518  symggrp  18522  symgextsymg  18546  gsmsymgreqlem2  18553  symgfixfolem1  18560  pmtrprfv3  18576  symggen  18592  lsmass  18789  efgsrel  18854  cntzcmn  18954  dvrcl  19430  unitdvcl  19431  dvrcan1  19435  subrgmre  19553  abvsubtri  19600  abvtrivd  19605  lmodvsubval2  19683  rmodislmodlem  19695  rmodislmod  19696  lss0cl  19712  lssintcl  19730  lssincl  19731  reslmhm2  19819  lspvadd  19862  lspsntrim  19864  islbs3  19921  rrgeq0  20057  evlsval2  20294  cncrng  20560  xrsmcmn  20562  cndrng  20568  cnsrng  20573  xrs1mnd  20577  absabv  20596  psgnco  20721  zrhpsgninv  20723  zrhpsgnevpm  20729  zrhpsgnodpm  20730  zrhpsgnelbas  20732  zrhcopsgnelbas  20733  uvcresum  20931  lindfmm  20965  lindsmm  20966  mamudm  20993  mamufacex  20994  matsubgcell  21037  matsc  21053  scmatscmide  21110  scmatrhmcl  21131  1marepvsma1  21186  m1detdiag  21200  mdetralt  21211  m2detleiblem7  21230  gsummatr01lem3  21260  gsummatr01  21262  smadiadetlem0  21264  decpmate  21368  decpmatcl  21369  pm2mpcl  21399  pm2mpghmlem2  21414  chfacfscmul0  21460  chfacfscmulgsum  21462  chfacfpmmul0  21464  chfacfpmmulgsum  21466  unopn  21505  clsss  21656  cldmre  21680  toponmre  21695  opnssneib  21717  restabs  21767  restcls  21783  restntr  21784  hausnei2  21955  cmpsublem  22001  bwth  22012  hausmapdom  22102  ptpjcn  22213  upxp  22225  ptrescn  22241  xkopjcn  22258  fbssfi  22439  snfil  22466  ufprim  22511  rnelfm  22555  flimrest  22585  fclsrest  22626  tmdgsum  22697  blpnfctr  23040  mscl  23065  xmscl  23066  xmsge0  23067  xmseq0  23068  restmetu  23174  ngpds  23207  tngngp3  23259  unitnmn0  23271  xrsxmet  23411  metds0  23452  cncfmptc  23513  isclmp  23695  cnlmod  23738  ncvsi  23749  cphsqrtcl  23782  cfil3i  23866  cfilres  23893  cmssmscld  23947  cmmbl  24129  voliunlem2  24146  itg2ub  24328  itgrecl  24392  tdeglem3  24647  r1pid  24747  eflogeq  25179  cxpadd  25256  cxpcom  25314  logbchbase  25343  relogbreexp  25347  relogbzexp  25348  relogbmulexp  25350  logbleb  25355  logblt  25356  lawcos  25388  pythag  25389  asinsinb  25469  acoscosb  25470  atantanb  25496  amgmlem  25561  lgsneg  25891  lgsne0  25905  lgsmodeq  25912  lgsmulsqcoprm  25913  gausslemma2dlem1a  25935  2sqreulem2  26022  brbtwn2  26685  colinearalg  26690  eleesubd  26692  axcgrrflx  26694  axcgrtr  26695  axsegcon  26707  ax5seglem1  26708  ax5seglem2  26709  ax5seglem4  26712  axbtwnid  26719  axlowdimlem14  26735  axlowdim  26741  axcontlem5  26748  axcontlem7  26750  nb3grprlem2  27157  cplgr3v  27211  cusgrsizeindslem  27227  sizusglecusglem2  27238  umgr2v2e  27301  cusgrrusgr  27357  iswlk  27386  edginwlk  27410  uspgr2wlkeq  27421  uspgr2wlkeq2  27422  uspgr2wlkeqi  27423  wlkonprop  27434  wlkon2n0  27442  pthdadjvtx  27505  upgr2pthnlp  27507  spthonepeq  27527  pthdlem2lem  27542  crctcshwlkn0lem3  27584  crctcshwlkn0lem5  27586  wlkiswwlks2lem4  27644  wlkiswwlks2lem6  27646  wlklnwwlkln2lem  27654  wwlksnred  27664  wwlksnextbi  27666  wwlksnextwrd  27669  2pthdlem1  27703  2wlkdlem10  27708  umgr2adedgwlkonALT  27720  elwwlks2s3  27724  elwwlks2ons3im  27727  s3wwlks2on  27729  2wspdisj  27735  2wspiundisj  27736  clwwlkgt0  27758  clwlkclwwlklem2a4  27769  clwlkclwwlklem2a  27770  clwlkclwwlk  27774  clwlkclwwlk2  27775  clwlkclwwlkfo  27781  clwwisshclwwslemlem  27785  erclwwlktr  27794  clwwlkf  27820  wwlksubclwwlk  27831  erclwwlkntr  27844  clwwlknon  27863  frcond1  28039  frgr3v  28048  3vfriswmgr  28051  frgrwopreglem4a  28083  frrusgrord0lem  28112  clwwnonrepclwwnon  28118  extwwlkfab  28125  numclwwlk1lem2f1  28130  numclwwlk1lem2fo  28131  clwlknon2num  28141  numclwwlk2lem1  28149  numclwlk2lem2f  28150  numclwlk2lem2f1o  28152  numclwwlk2  28154  frgrreggt1  28166  friendshipgt3  28171  imsmetlem  28461  nmoxr  28537  nmoolb  28542  blometi  28574  phpar2  28594  phpar  28595  ipasslem5  28606  hvadd32  28805  hvaddsub12  28809  hvaddsubass  28812  hvsubass  28815  hvsub32  28816  hvsubdistr1  28820  hvsubdistr2  28821  hvmulcan  28843  hvmulcan2  28844  hvsubcan  28845  his5  28857  his2sub  28863  hhssabloilem  29032  hhssnv  29035  shlej2  29132  pjoi0  29488  hodcl  29518  hoadd32  29554  hosubdi  29579  hosubsub2  29583  hoaddsubass  29586  hosubsub4  29589  nmoplb  29678  unop  29686  hmop  29693  nmfnlb  29695  lnopmul  29738  kbass1  29887  kbass2  29888  leopmul2i  29906  leoptr  29908  cvntr  30063  mdslmd4i  30104  mdexchi  30106  atcv1  30151  sumdmdii  30186  fcoinvbr  30352  fpwrelmapffs  30464  xreceu  30593  isinftm  30805  unitdivcld  31139  esummulc1  31335  hasheuni  31339  unelsiga  31388  inelpisys  31408  carsgsigalem  31568  signswmnd  31822  bnj545  32162  bnj594  32179  bnj1311  32291  hashf1dmcdm  32351  usgrgt2cycl  32372  subgrwlk  32374  acycgr1v  32391  cvmsf1o  32514  cvmscld  32515  satefvfmla1  32667  elnanelprv  32671  lediv2aALT  32915  gcd32  32978  fununiq  33007  trpredpo  33069  poseq  33090  frr3g  33116  sltres  33164  sltletr  33230  sletr  33232  nocvxmin  33243  dfrdg4  33407  brcolinear  33515  colinearex  33516  nn0prpwlem  33665  clsun  33671  fnemeet1  33709  fnemeet2  33710  fnejoin1  33711  fnejoin2  33712  eltail  33717  rdgeqoa  34645  nlpineqsn  34683  curf  34864  lindsadd  34879  poimirlem28  34914  cnambfre  34934  ftc1anclem4  34964  cocanfo  34987  f1ocan1fv  34995  metf1o  35024  ismtybnd  35079  ghomco  35163  isdrngo2  35230  inidl  35302  igenmin  35336  brxrn  35620  brredunds  35855  cmtvalN  36341  cvrval  36399  pmapmeet  36903  paddval  36928  paddssat  36944  elpcliN  37023  pclssN  37024  pclunN  37028  paddunN  37057  poldmj1N  37058  tendoplcl2  37908  tendoplcl  37911  dihmeet  38473  expgcd  39176  zexpgcd  39178  reltsub1  39209  reltsubadd2  39210  resubsub4  39212  reppncan  39216  resubdi  39219  readdcan2  39235  mapco2g  39304  mzpcompact2lem  39341  eqrabdioph  39367  lerabdioph  39395  eluzrabdioph  39396  ltrabdioph  39398  nerabdioph  39399  dvdsrabdioph  39400  reglogcl  39480  rmxyadd  39511  rmyabs  39548  congadd  39556  congabseq  39564  rmydioph  39604  mendring  39785  mendlmod  39786  iocinico  39811  relexp0a  40054  relexpaddss  40056  brcoffn  40373  dvconstbi  40659  uzwo4  41308  ssin0  41310  ssinc  41346  ssdec  41347  fvmpt2bd  41418  disjf1o  41444  ssnnf1octb  41448  sub31  41549  fperiodmullem  41562  ssfiunibd  41568  infxr  41627  fmul01  41853  islptre  41892  lptre2pt  41913  limcleqr  41917  limclner  41924  limsuppnflem  41983  limsupvaluz2  42011  supcnvlimsup  42013  xlimmnfvlem2  42106  xlimmnfv  42107  xlimpnfvlem2  42110  xlimpnfv  42111  climxlim2lem  42118  coskpi2  42139  cosknegpi  42142  dvnmptdivc  42215  dvdsn1add  42216  dvnmptconst  42218  dvmptfprod  42222  dvnprodlem1  42223  dvnprodlem2  42224  ovolsplit  42266  stoweidlem60  42338  stowei  42342  dirkeritg  42380  fourierdlem70  42454  fourierdlem71  42455  fourierdlem103  42487  fourierdlem104  42488  fouriersw  42509  rrxtopnfi  42565  saluncl  42595  salexct  42610  sge0ltfirp  42675  sge0iunmpt  42693  meadjiunlem  42740  meaiuninc3v  42759  carageniuncllem1  42796  caratheodorylem1  42801  ovncvrrp  42839  ovnsubaddlem1  42845  hspmbllem2  42902  ovolval5lem3  42929  smfpimbor1lem1  43066  smfsuplem1  43078  smflimsuplem4  43090  sigarls  43107  cnambpcma  43487  elfzelfzlble  43514  fzoopth  43520  m1mod0mod1  43522  fsumsplitsndif  43526  fundcmpsurinjALT  43565  iccpartiltu  43575  prproropf1olem2  43659  fmtno4prmfac  43727  2pwp1prmfmtno  43745  lighneallem4b  43767  mogoldbblem  43878  gbegt5  43919  sbgoldbm  43942  nnsum3primesle9  43952  nnsum4primesodd  43954  nnsum4primesoddALTV  43955  evengpoap3  43957  nnsum4primesevenALTV  43959  isomgrtr  43997  strisomgrop  43998  isupwlk  44004  lidldomnnring  44194  2zrngacmnd  44206  rhmsubclem2  44351  rhmsubcALTVlem2  44369  zlmodzxzscm  44398  gsumlsscl  44424  lincvalsng  44464  lincvalpr  44466  lincdifsn  44472  linc1  44473  lincellss  44474  difmodm1lt  44575  fdivmpt  44593  digexp  44660  line  44712  rrxline  44714  itsclc0xyqsolr  44749  amgmwlem  44896