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  2632  spc3egv  3554  sbciegftOLD  3775  reuhyp  5362  predtrss  6276  onunel  6420  funopg  6522  funprg  6542  funtpg  6543  funcnvtp  6551  unima  6905  fvun1  6921  fnreseql  6989  xpprsng  7081  ftpg  7097  f1ounsn  7214  f13dfv  7216  f1ocoima  7245  f1ofvswap  7248  mpoeq3ia  7432  ordunel  7765  fex2  7874  funexw  7892  poxp  8066  poxp2  8081  poxp3  8088  poseq  8096  suppval1  8104  wfr3g  8257  smores3  8281  oaord  8470  oacan  8471  oaword  8472  omord  8491  omcan  8492  omwordri  8495  odi  8502  omass  8503  oeord  8511  oecan  8512  oewordri  8515  oeordsuc  8517  nnaord  8542  nnaordr  8543  nndi  8546  nnmass  8547  nnaword  8550  nnmord  8555  nnmwordri  8559  naddelim  8609  naddel1  8610  naddel2  8611  naddss1  8612  naddss2  8613  naddasslem2  8618  nadd32  8620  erov  8746  ecopovtrn  8752  ixpf  8852  f1oen4g  8895  f1dom4g  8896  mapxpen  9065  ssfi  9091  sbthfilem  9116  sbthfi  9117  onomeneq  9132  fimax2g  9179  unbnn  9189  funisfsupp  9260  inelfi  9311  elfiun  9323  sup0  9360  suppr  9365  infpr  9398  ttrclss  9619  frr3g  9658  r111  9677  dif1card  9910  ackbij1lem16  10134  cff1  10158  cfflb  10159  cfsmolem  10170  fin23lem34  10246  hsmexlem2  10327  axcc3  10338  domtriomlem  10342  axdc3lem4  10353  axdc4lem  10355  axcclem  10357  konigthlem  10468  gchdomtri  10529  tskpr  10670  tskop  10671  tskuni  10683  tskun  10686  gruop  10705  gruun  10706  grudomon  10717  adderpqlem  10854  mulerpqlem  10855  addassnq  10858  mulassnq  10859  distrnq  10861  ltsonq  10869  ltanq  10871  ltmnq  10872  genpass  10909  distrlem1pr  10925  distrlem4pr  10926  ltsopr  10932  adddir  11112  axlttrn  11194  ltletr  11214  letr  11216  mul32  11288  mul31  11289  add32  11341  subsub23  11374  addsubass  11379  subcan2  11395  subsub2  11398  nppcan2  11401  sub32  11404  nnncan  11405  nnncan2  11407  pnpcan2  11410  subdi  11559  subdir  11560  receu  11771  mulcan1g  11779  mulcan2g  11780  divmul3  11790  divrec  11801  divrec2  11802  div11  11813  divsubdir  11824  subdivcomb2  11826  divdiv1  11841  redivcl  11849  div2neg  11853  ltmul2  11981  lemul1  11982  lemul2  11983  lemul2a  11985  lediv1  11996  gt0div  11997  ge0div  11998  mulsuble0b  12003  ltdivmul  12006  ledivmul  12007  ltdivmul2  12008  ledivmul2  12010  lemuldiv  12011  ltdiv23  12022  lediv23  12023  ledivp1i  12056  ltdivp1i  12057  uzind2  12574  nn0ind  12576  fnn0ind  12580  uz3m2nn  12796  xrltletr  13060  xrletr  13061  xrre2  13073  xrltmin  13085  xrlemin  13087  xleadd2a  13157  xleadd1  13158  xltadd2  13160  xmulasslem3  13189  xmulass  13190  xltmul2  13196  ixxdisj  13264  iooneg  13375  iccneg  13376  icoshft  13377  icoshftf1o  13378  icodisj  13380  snunioo  13382  fzen  13445  ssfzunsnext  13473  fzrev3  13494  2ffzeq  13553  fzoaddel2  13624  elfzodifsumelfzo  13635  ssfzoulel  13664  ssfzo12bi  13665  fzoopth  13666  fzoshftral  13691  adddivflid  13726  flltdivnn0lt  13741  ltdifltdiv  13742  fldiv4p1lem1div2  13743  modcyc  13814  modcyc2  13815  modaddabs  13819  muladdmod  13823  modsubmodmod  13841  modaddmodup  13845  modaddmulmod  13849  moddi  13850  modsubdir  13851  expdiv  14024  digit2  14147  nfile  14270  hashdifpr  14326  hashgt23el  14335  hashreshashfun  14350  hashf1dmcdm  14355  hash3tpexb  14405  fi1uzind  14418  ccatval1  14488  ccatass  14500  swrdval  14555  swrdnd  14566  swrd0  14570  swrdfv2  14573  pfxsuff1eqwrdeq  14610  swrdswrdlem  14615  pfxccatin12lem2a  14638  pfxccatin12lem1  14639  repswccat  14697  cshwidxmod  14714  cshwidxmodr  14715  cshf1  14721  repswcshw  14723  2cshw  14724  2cshwcom  14727  2cshwcshw  14736  cshwcsh2id  14739  ccatco  14746  2swrd2eqwrdeq  14864  wwlktovf  14867  brcnvtrclfv  14914  shftval2  14986  mulre  15032  absdiv  15206  absdiflt  15229  absdifle  15230  abs3dif  15243  cau3  15267  ello12r  15428  elo12r  15439  modfsummods  15704  geoisum1c  15791  rpnnen2lem4  16130  rpnnen2lem7  16133  addmulmodb  16180  dvdsmulc  16198  dvdsmulcr  16200  dvdsmultr1  16211  dvdsmultr2  16213  dvdssub2  16216  oexpneg  16260  divalgb  16319  ndvdsadd  16325  sadass  16386  modgcd  16447  dvdsgcd  16459  dvdsgcdb  16460  gcdass  16462  mulgcd  16463  absmulgcd  16464  rpmulgcd  16472  expgcd  16478  zexpgcd  16480  nn0seqcvgd  16485  algcvga  16494  lcmdvdsb  16528  lcmass  16529  lcmfunsnlem1  16552  lcmfunsnlem2lem1  16553  lcmfunsnlem2lem2  16554  coprmdvds  16568  coprmdvds2  16569  rpmul  16574  cncongr1  16582  cncongr2  16583  qnumdenbi  16659  modprm0  16721  coprimeprodsq  16724  pythagtriplem4  16735  pythagtriplem8  16739  pythagtriplem9  16740  pythagtriplem12  16742  pythagtriplem14  16744  pythagtriplem16  16746  pcpremul  16759  pcgcd  16794  vdwapval  16889  vdwapun  16890  prmgaplem3  16969  prmgaplem4  16970  prmgaplem7  16973  prmgapprmolem  16977  mreiincl  17502  mreincl  17505  mremre  17510  mrcss  17526  catcisolem  18021  pleval2  18245  pospo  18253  latlem  18347  latjcom  18357  latmcom  18373  lubss  18423  lubun  18425  clatglbss  18429  ipole  18444  ipolt  18445  pslem  18482  dirtr  18512  gsumsgrpccat  18752  gsumws2  18754  frmdmnd  18771  symggrplem  18796  isgrpi  18876  grpsubrcan  18938  grpinvsub  18939  grpsubeq0  18943  grpsubadd0sub  18944  grpnpcan  18949  qussub  19107  ghmsub  19140  symgpssefmnd  19312  symggrp  19316  symgextsymg  19340  gsmsymgreqlem2  19347  symgfixfolem1  19354  pmtrprfv3  19370  symggen  19386  lsmass  19585  efgsrel  19650  cntzcmn  19756  dvrcl  20326  unitdvcl  20327  dvrcan1  20331  subrngmre  20481  subrgmre  20516  rhmsubclem2  20605  rrgeq0  20619  abvsubtri  20746  abvtrivd  20751  lmodvsubval2  20854  rmodislmodlem  20866  rmodislmod  20867  lss0cl  20884  lssintcl  20901  lssincl  20902  reslmhm2  20991  lspvadd  21034  lspsntrim  21036  islbs3  21096  rnglidlmmgm  21186  cncrng  21329  cncrngOLD  21330  xrsmcmn  21332  cndrng  21339  cndrngOLD  21340  cnsrng  21346  absabv  21365  xrs1mnd  21381  psgnco  21524  zrhpsgninv  21526  zrhpsgnevpm  21532  zrhpsgnodpm  21533  zrhpsgnelbas  21535  zrhcopsgnelbas  21536  uvcresum  21734  lindfmm  21768  lindsmm  21769  evlsval2  22025  mamudm  22313  mamufacex  22314  matsubgcell  22352  matsc  22368  scmatscmide  22425  scmatrhmcl  22446  1marepvsma1  22501  m1detdiag  22515  mdetralt  22526  m2detleiblem7  22545  gsummatr01lem3  22575  gsummatr01  22577  smadiadetlem0  22579  decpmate  22684  decpmatcl  22685  pm2mpcl  22715  pm2mpghmlem2  22730  chfacfscmul0  22776  chfacfscmulgsum  22778  chfacfpmmul0  22780  chfacfpmmulgsum  22782  unopn  22821  clsss  22972  cldmre  22996  toponmre  23011  opnssneib  23033  restabs  23083  restcls  23099  restntr  23100  hausnei2  23271  cmpsublem  23317  bwth  23328  hausmapdom  23418  ptpjcn  23529  upxp  23541  ptrescn  23557  xkopjcn  23574  fbssfi  23755  snfil  23782  ufprim  23827  rnelfm  23871  flimrest  23901  fclsrest  23942  tmdgsum  24013  blpnfctr  24354  mscl  24379  xmscl  24380  xmsge0  24381  xmseq0  24382  restmetu  24488  ngpds  24522  tngngp3  24574  unitnmn0  24586  xrsxmet  24728  metds0  24769  mpomulcn  24788  cncfmptc  24835  isclmp  25027  cnlmod  25070  ncvsi  25081  cphsqrtcl  25114  cfil3i  25199  cfilres  25226  cmssmscld  25280  cmmbl  25465  voliunlem2  25482  itg2ub  25664  itgrecl  25729  r1pid  26096  eflogeq  26541  cxpadd  26618  cxpcom  26678  logbchbase  26711  relogbreexp  26715  relogbzexp  26716  relogbmulexp  26718  logbleb  26723  logblt  26724  lawcos  26756  pythag  26757  asinsinb  26837  acoscosb  26838  atantanb  26864  amgmlem  26930  lgsneg  27262  lgsne0  27276  lgsmodeq  27283  lgsmulsqcoprm  27284  gausslemma2dlem1a  27306  2sqreulem2  27393  sltres  27604  noetainflem1  27679  sltletr  27698  sletr  27700  nocvxmin  27721  madebdaylemold  27846  lrrecpo  27887  sltadd2im  27932  sleadd1im  27933  sleadd2im  27934  sleadd1  27935  sleadd2  27936  sltadd1  27938  addscan2  27939  addscan1  27940  subadds  28013  sltsub1  28019  divscl  28164  onscutlt  28204  zsoring  28335  expscllem  28356  0reno  28402  brbtwn2  28887  colinearalg  28892  eleesubd  28894  axcgrrflx  28896  axcgrtr  28897  axsegcon  28909  ax5seglem1  28910  ax5seglem2  28911  ax5seglem4  28914  axbtwnid  28921  axlowdimlem14  28937  axlowdim  28943  axcontlem5  28950  axcontlem7  28952  nb3grprlem2  29363  cplgr3v  29417  cusgrsizeindslem  29434  sizusglecusglem2  29445  umgr2v2e  29508  cusgrrusgr  29564  iswlk  29593  edginwlk  29617  uspgr2wlkeq  29628  uspgr2wlkeq2  29629  uspgr2wlkeqi  29630  wlkonprop  29639  wlkon2n0  29647  pthdadjvtx  29710  upgr2pthnlp  29714  spthonepeq  29734  pthdlem2lem  29749  crctcshwlkn0lem3  29794  crctcshwlkn0lem5  29796  wlkiswwlks2lem4  29854  wlkiswwlks2lem6  29856  wlklnwwlkln2lem  29864  wwlksnred  29874  wwlksnextbi  29876  wwlksnextwrd  29879  2pthdlem1  29912  2wlkdlem10  29917  umgr2adedgwlkonALT  29929  elwwlks2s3  29933  elwwlks2ons3im  29936  s3wwlks2on  29938  sps3wwlks2on  29939  2wspdisj  29947  2wspiundisj  29948  clwwlkgt0  29970  clwlkclwwlklem2a4  29981  clwlkclwwlklem2a  29982  clwlkclwwlk  29986  clwlkclwwlk2  29987  clwlkclwwlkfo  29993  clwwisshclwwslemlem  29997  erclwwlktr  30006  clwwlkf  30031  wwlksubclwwlk  30042  erclwwlkntr  30055  clwwlknon  30074  frcond1  30250  frgr3v  30259  3vfriswmgr  30262  frgrwopreglem4a  30294  frrusgrord0lem  30323  clwwnonrepclwwnon  30329  extwwlkfab  30336  numclwwlk1lem2f1  30341  numclwwlk1lem2fo  30342  clwlknon2num  30352  numclwwlk2lem1  30360  numclwlk2lem2f  30361  numclwlk2lem2f1o  30363  numclwwlk2  30365  frgrreggt1  30377  friendshipgt3  30382  imsmetlem  30674  nmoxr  30750  nmoolb  30755  blometi  30787  phpar2  30807  phpar  30808  ipasslem5  30819  hvadd32  31018  hvaddsub12  31022  hvaddsubass  31025  hvsubass  31028  hvsub32  31029  hvsubdistr1  31033  hvsubdistr2  31034  hvmulcan  31056  hvmulcan2  31057  hvsubcan  31058  his5  31070  his2sub  31076  hhssabloilem  31245  hhssnv  31248  shlej2  31345  pjoi0  31701  hodcl  31731  hoadd32  31767  hosubdi  31792  hosubsub2  31796  hoaddsubass  31799  hosubsub4  31802  nmoplb  31891  unop  31899  hmop  31906  nmfnlb  31908  lnopmul  31951  kbass1  32100  kbass2  32101  leopmul2i  32119  leoptr  32121  cvntr  32276  mdslmd4i  32317  mdexchi  32319  atcv1  32364  sumdmdii  32399  fcoinvbr  32589  fpwrelmapffs  32723  xreceu  32911  isinftm  33159  unitdivcld  33937  esummulc1  34117  hasheuni  34121  unelsiga  34170  inelpisys  34190  carsgsigalem  34351  signswmnd  34593  bnj545  34930  bnj594  34947  bnj1311  35059  fissorduni  35124  r1filimi  35137  fineqvac  35162  fineqvnttrclselem3  35166  usgrgt2cycl  35197  subgrwlk  35199  acycgr1v  35216  cvmsf1o  35339  cvmscld  35340  satefvfmla1  35492  elnanelprv  35496  lediv2aALT  35744  gcd32  35816  fununiq  35836  dfrdg4  36018  brcolinear  36126  colinearex  36127  nn0prpwlem  36389  clsun  36395  fnemeet1  36433  fnemeet2  36434  fnejoin1  36435  fnejoin2  36436  eltail  36441  rdgeqoa  37437  nlpineqsn  37475  curf  37661  lindsadd  37676  poimirlem28  37711  cnambfre  37731  ftc1anclem4  37759  cocanfo  37782  f1ocan1fv  37789  metf1o  37818  ismtybnd  37870  ghomco  37954  isdrngo2  38021  inidl  38093  igenmin  38127  brxrn  38430  brredunds  38745  cmtvalN  39333  cvrval  39391  pmapmeet  39895  paddval  39920  paddssat  39936  elpcliN  40015  pclssN  40016  pclunN  40020  paddunN  40049  poldmj1N  40050  tendoplcl2  40900  tendoplcl  40903  dihmeet  41465  lcmineqlem1  42145  reltsub1  42507  reltsubadd2  42508  resubsub4  42510  reppncan  42514  resubdi  42517  readdcan2  42534  subresre  42552  mapco2g  42834  mzpcompact2lem  42871  eqrabdioph  42897  lerabdioph  42925  eluzrabdioph  42926  ltrabdioph  42928  nerabdioph  42929  dvdsrabdioph  42930  reglogcl  43010  rmxyadd  43041  rmyabs  43078  congadd  43086  congabseq  43094  rmydioph  43134  mendring  43308  mendlmod  43309  iocinico  43332  omge1  43417  relexp0a  43836  relexpaddss  43838  brcoffn  44150  ismnushort  44421  dvconstbi  44454  uzwo4  45177  ssin0  45179  ssinc  45211  ssdec  45212  fvmpt2bd  45294  disjf1o  45315  ssnnf1octb  45318  sub31  45418  fperiodmullem  45431  ssfiunibd  45437  infxr  45492  fmul01  45707  islptre  45746  lptre2pt  45765  limcleqr  45769  limclner  45776  limsuppnflem  45835  limsupvaluz2  45863  supcnvlimsup  45865  xlimmnfvlem2  45958  xlimmnfv  45959  xlimpnfvlem2  45962  xlimpnfv  45963  climxlim2lem  45970  coskpi2  45991  cosknegpi  45994  dvnmptdivc  46063  dvdsn1add  46064  dvnmptconst  46066  dvmptfprod  46070  dvnprodlem1  46071  dvnprodlem2  46072  ovolsplit  46113  stoweidlem60  46185  stowei  46189  dirkeritg  46227  fourierdlem70  46301  fourierdlem71  46302  fourierdlem103  46334  fourierdlem104  46335  fouriersw  46356  rrxtopnfi  46412  saluncl  46442  salexct  46459  sge0ltfirp  46525  sge0iunmpt  46543  meadjiunlem  46590  meaiuninc3v  46609  carageniuncllem1  46646  caratheodorylem1  46651  ovncvrrp  46689  ovnsubaddlem1  46695  hspmbllem2  46752  ovolval5lem3  46779  smfpimbor1lem1  46923  smfsuplem1  46936  smflimsuplem4  46948  sigarls  46982  cnambpcma  47421  elfzelfzlble  47448  submodaddmod  47468  difltmodne  47469  m1mod0mod1  47481  modmkpkne  47488  mod2addne  47491  modm2nep1  47493  modm1nep2  47495  modm1nem2  47496  fsumsplitsndif  47500  fundcmpsurinjALT  47539  iccpartiltu  47549  prproropf1olem2  47631  fmtno4prmfac  47699  2pwp1prmfmtno  47717  lighneallem4b  47736  mogoldbblem  47847  gbegt5  47888  sbgoldbm  47911  nnsum3primesle9  47921  nnsum4primesodd  47923  nnsum4primesoddALTV  47924  evengpoap3  47926  nnsum4primesevenALTV  47928  clnbgredg  47967  opstrgric  48053  clnbgrgrimlem  48060  grtrif1o  48069  isubgr3stgrlem1  48093  isubgr3stgrlem4  48096  gpgusgralem  48183  gpg3nbgrvtx0  48203  isupwlk  48263  lidldomnnring  48363  2zrngacmnd  48375  rhmsubcALTVlem2  48409  fprmappr  48472  zlmodzxzscm  48484  gsumlsscl  48507  lincvalsng  48544  lincvalpr  48546  lincdifsn  48552  linc1  48553  lincellss  48554  fdivmpt  48668  digexp  48735  2arymaptfo  48782  line  48860  rrxline  48862  itsclc0xyqsolr  48897  iscnrm3r  49075  resipos  49102  amgmwlem  49930