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  3555  sbciegftOLD  3776  reuhyp  5362  predtrss  6277  onunel  6421  funopg  6523  funprg  6543  funtpg  6544  funcnvtp  6552  unima  6906  fvun1  6922  fnreseql  6990  xpprsng  7082  ftpg  7098  f1ounsn  7215  f13dfv  7217  f1ocoima  7246  f1ofvswap  7249  mpoeq3ia  7433  ordunel  7766  fex2  7875  funexw  7893  poxp  8067  poxp2  8082  poxp3  8089  poseq  8097  suppval1  8105  wfr3g  8258  smores3  8282  oaord  8471  oacan  8472  oaword  8473  omord  8492  omcan  8493  omwordri  8496  odi  8503  omass  8504  oeord  8512  oecan  8513  oewordri  8516  oeordsuc  8518  nnaord  8543  nnaordr  8544  nndi  8547  nnmass  8548  nnaword  8551  nnmord  8556  nnmwordri  8560  naddelim  8610  naddel1  8611  naddel2  8612  naddss1  8613  naddss2  8614  naddasslem2  8619  nadd32  8621  erov  8747  ecopovtrn  8753  ixpf  8853  f1oen4g  8896  f1dom4g  8897  mapxpen  9066  ssfi  9092  sbthfilem  9117  sbthfi  9118  onomeneq  9133  fimax2g  9180  unbnn  9190  funisfsupp  9261  inelfi  9312  elfiun  9324  sup0  9361  suppr  9366  infpr  9399  ttrclss  9620  frr3g  9659  r111  9678  dif1card  9911  ackbij1lem16  10135  cff1  10159  cfflb  10160  cfsmolem  10171  fin23lem34  10247  hsmexlem2  10328  axcc3  10339  domtriomlem  10343  axdc3lem4  10354  axdc4lem  10356  axcclem  10358  konigthlem  10469  gchdomtri  10530  tskpr  10671  tskop  10672  tskuni  10684  tskun  10687  gruop  10706  gruun  10707  grudomon  10718  adderpqlem  10855  mulerpqlem  10856  addassnq  10859  mulassnq  10860  distrnq  10862  ltsonq  10870  ltanq  10872  ltmnq  10873  genpass  10910  distrlem1pr  10926  distrlem4pr  10927  ltsopr  10933  adddir  11113  axlttrn  11195  ltletr  11215  letr  11217  mul32  11289  mul31  11290  add32  11342  subsub23  11375  addsubass  11380  subcan2  11396  subsub2  11399  nppcan2  11402  sub32  11405  nnncan  11406  nnncan2  11408  pnpcan2  11411  subdi  11560  subdir  11561  receu  11772  mulcan1g  11780  mulcan2g  11781  divmul3  11791  divrec  11802  divrec2  11803  div11  11814  divsubdir  11825  subdivcomb2  11827  divdiv1  11842  redivcl  11850  div2neg  11854  ltmul2  11982  lemul1  11983  lemul2  11984  lemul2a  11986  lediv1  11997  gt0div  11998  ge0div  11999  mulsuble0b  12004  ltdivmul  12007  ledivmul  12008  ltdivmul2  12009  ledivmul2  12011  lemuldiv  12012  ltdiv23  12023  lediv23  12024  ledivp1i  12057  ltdivp1i  12058  uzind2  12576  nn0ind  12578  fnn0ind  12582  uz3m2nn  12802  xrltletr  13066  xrletr  13067  xrre2  13079  xrltmin  13091  xrlemin  13093  xleadd2a  13163  xleadd1  13164  xltadd2  13166  xmulasslem3  13195  xmulass  13196  xltmul2  13202  ixxdisj  13270  iooneg  13381  iccneg  13382  icoshft  13383  icoshftf1o  13384  icodisj  13386  snunioo  13388  fzen  13451  ssfzunsnext  13479  fzrev3  13500  2ffzeq  13559  fzoaddel2  13630  elfzodifsumelfzo  13641  ssfzoulel  13670  ssfzo12bi  13671  fzoopth  13672  fzoshftral  13697  adddivflid  13732  flltdivnn0lt  13747  ltdifltdiv  13748  fldiv4p1lem1div2  13749  modcyc  13820  modcyc2  13821  modaddabs  13825  muladdmod  13829  modsubmodmod  13847  modaddmodup  13851  modaddmulmod  13855  moddi  13856  modsubdir  13857  expdiv  14030  digit2  14153  nfile  14276  hashdifpr  14332  hashgt23el  14341  hashreshashfun  14356  hashf1dmcdm  14361  hash3tpexb  14411  fi1uzind  14424  ccatval1  14494  ccatass  14506  swrdval  14561  swrdnd  14572  swrd0  14576  swrdfv2  14579  pfxsuff1eqwrdeq  14616  swrdswrdlem  14621  pfxccatin12lem2a  14644  pfxccatin12lem1  14645  repswccat  14703  cshwidxmod  14720  cshwidxmodr  14721  cshf1  14727  repswcshw  14729  2cshw  14730  2cshwcom  14733  2cshwcshw  14742  cshwcsh2id  14745  ccatco  14752  2swrd2eqwrdeq  14870  wwlktovf  14873  brcnvtrclfv  14920  shftval2  14992  mulre  15038  absdiv  15212  absdiflt  15235  absdifle  15236  abs3dif  15249  cau3  15273  ello12r  15434  elo12r  15445  modfsummods  15710  geoisum1c  15797  rpnnen2lem4  16136  rpnnen2lem7  16139  addmulmodb  16186  dvdsmulc  16204  dvdsmulcr  16206  dvdsmultr1  16217  dvdsmultr2  16219  dvdssub2  16222  oexpneg  16266  divalgb  16325  ndvdsadd  16331  sadass  16392  modgcd  16453  dvdsgcd  16465  dvdsgcdb  16466  gcdass  16468  mulgcd  16469  absmulgcd  16470  rpmulgcd  16478  expgcd  16484  zexpgcd  16486  nn0seqcvgd  16491  algcvga  16500  lcmdvdsb  16534  lcmass  16535  lcmfunsnlem1  16558  lcmfunsnlem2lem1  16559  lcmfunsnlem2lem2  16560  coprmdvds  16574  coprmdvds2  16575  rpmul  16580  cncongr1  16588  cncongr2  16589  qnumdenbi  16665  modprm0  16727  coprimeprodsq  16730  pythagtriplem4  16741  pythagtriplem8  16745  pythagtriplem9  16746  pythagtriplem12  16748  pythagtriplem14  16750  pythagtriplem16  16752  pcpremul  16765  pcgcd  16800  vdwapval  16895  vdwapun  16896  prmgaplem3  16975  prmgaplem4  16976  prmgaplem7  16979  prmgapprmolem  16983  mreiincl  17508  mreincl  17511  mremre  17516  mrcss  17532  catcisolem  18027  pleval2  18251  pospo  18259  latlem  18353  latjcom  18363  latmcom  18379  lubss  18429  lubun  18431  clatglbss  18435  ipole  18450  ipolt  18451  pslem  18488  dirtr  18518  gsumsgrpccat  18758  gsumws2  18760  frmdmnd  18777  symggrplem  18802  isgrpi  18882  grpsubrcan  18944  grpinvsub  18945  grpsubeq0  18949  grpsubadd0sub  18950  grpnpcan  18955  qussub  19113  ghmsub  19146  symgpssefmnd  19318  symggrp  19322  symgextsymg  19346  gsmsymgreqlem2  19353  symgfixfolem1  19360  pmtrprfv3  19376  symggen  19392  lsmass  19591  efgsrel  19656  cntzcmn  19762  dvrcl  20332  unitdvcl  20333  dvrcan1  20337  subrngmre  20487  subrgmre  20522  rhmsubclem2  20611  rrgeq0  20625  abvsubtri  20752  abvtrivd  20757  lmodvsubval2  20860  rmodislmodlem  20872  rmodislmod  20873  lss0cl  20890  lssintcl  20907  lssincl  20908  reslmhm2  20997  lspvadd  21040  lspsntrim  21042  islbs3  21102  rnglidlmmgm  21192  cncrng  21335  cncrngOLD  21336  xrsmcmn  21338  cndrng  21345  cndrngOLD  21346  cnsrng  21352  absabv  21371  xrs1mnd  21387  psgnco  21530  zrhpsgninv  21532  zrhpsgnevpm  21538  zrhpsgnodpm  21539  zrhpsgnelbas  21541  zrhcopsgnelbas  21542  uvcresum  21740  lindfmm  21774  lindsmm  21775  evlsval2  22032  mamudm  22320  mamufacex  22321  matsubgcell  22359  matsc  22375  scmatscmide  22432  scmatrhmcl  22453  1marepvsma1  22508  m1detdiag  22522  mdetralt  22533  m2detleiblem7  22552  gsummatr01lem3  22582  gsummatr01  22584  smadiadetlem0  22586  decpmate  22691  decpmatcl  22692  pm2mpcl  22722  pm2mpghmlem2  22737  chfacfscmul0  22783  chfacfscmulgsum  22785  chfacfpmmul0  22787  chfacfpmmulgsum  22789  unopn  22828  clsss  22979  cldmre  23003  toponmre  23018  opnssneib  23040  restabs  23090  restcls  23106  restntr  23107  hausnei2  23278  cmpsublem  23324  bwth  23335  hausmapdom  23425  ptpjcn  23536  upxp  23548  ptrescn  23564  xkopjcn  23581  fbssfi  23762  snfil  23789  ufprim  23834  rnelfm  23878  flimrest  23908  fclsrest  23949  tmdgsum  24020  blpnfctr  24361  mscl  24386  xmscl  24387  xmsge0  24388  xmseq0  24389  restmetu  24495  ngpds  24529  tngngp3  24581  unitnmn0  24593  xrsxmet  24735  metds0  24776  mpomulcn  24795  cncfmptc  24842  isclmp  25034  cnlmod  25077  ncvsi  25088  cphsqrtcl  25121  cfil3i  25206  cfilres  25233  cmssmscld  25287  cmmbl  25472  voliunlem2  25489  itg2ub  25671  itgrecl  25736  r1pid  26103  eflogeq  26548  cxpadd  26625  cxpcom  26685  logbchbase  26718  relogbreexp  26722  relogbzexp  26723  relogbmulexp  26725  logbleb  26730  logblt  26731  lawcos  26763  pythag  26764  asinsinb  26844  acoscosb  26845  atantanb  26871  amgmlem  26937  lgsneg  27269  lgsne0  27283  lgsmodeq  27290  lgsmulsqcoprm  27291  gausslemma2dlem1a  27313  2sqreulem2  27400  sltres  27611  noetainflem1  27686  sltletr  27705  sletr  27707  nocvxmin  27728  madebdaylemold  27853  lrrecpo  27894  sltadd2im  27939  sleadd1im  27940  sleadd2im  27941  sleadd1  27942  sleadd2  27943  sltadd1  27945  addscan2  27946  addscan1  27947  subadds  28020  sltsub1  28026  divscl  28171  onscutlt  28211  zsoring  28342  expscllem  28363  0reno  28409  brbtwn2  28894  colinearalg  28899  eleesubd  28901  axcgrrflx  28903  axcgrtr  28904  axsegcon  28916  ax5seglem1  28917  ax5seglem2  28918  ax5seglem4  28921  axbtwnid  28928  axlowdimlem14  28944  axlowdim  28950  axcontlem5  28957  axcontlem7  28959  nb3grprlem2  29370  cplgr3v  29424  cusgrsizeindslem  29441  sizusglecusglem2  29452  umgr2v2e  29515  cusgrrusgr  29571  iswlk  29600  edginwlk  29624  uspgr2wlkeq  29635  uspgr2wlkeq2  29636  uspgr2wlkeqi  29637  wlkonprop  29646  wlkon2n0  29654  pthdadjvtx  29717  upgr2pthnlp  29721  spthonepeq  29741  pthdlem2lem  29756  crctcshwlkn0lem3  29801  crctcshwlkn0lem5  29803  wlkiswwlks2lem4  29861  wlkiswwlks2lem6  29863  wlklnwwlkln2lem  29871  wwlksnred  29881  wwlksnextbi  29883  wwlksnextwrd  29886  2pthdlem1  29919  2wlkdlem10  29924  umgr2adedgwlkonALT  29936  elwwlks2s3  29940  elwwlks2ons3im  29943  s3wwlks2on  29945  sps3wwlks2on  29946  2wspdisj  29954  2wspiundisj  29955  clwwlkgt0  29977  clwlkclwwlklem2a4  29988  clwlkclwwlklem2a  29989  clwlkclwwlk  29993  clwlkclwwlk2  29994  clwlkclwwlkfo  30000  clwwisshclwwslemlem  30004  erclwwlktr  30013  clwwlkf  30038  wwlksubclwwlk  30049  erclwwlkntr  30062  clwwlknon  30081  frcond1  30257  frgr3v  30266  3vfriswmgr  30269  frgrwopreglem4a  30301  frrusgrord0lem  30330  clwwnonrepclwwnon  30336  extwwlkfab  30343  numclwwlk1lem2f1  30348  numclwwlk1lem2fo  30349  clwlknon2num  30359  numclwwlk2lem1  30367  numclwlk2lem2f  30368  numclwlk2lem2f1o  30370  numclwwlk2  30372  frgrreggt1  30384  friendshipgt3  30389  imsmetlem  30681  nmoxr  30757  nmoolb  30762  blometi  30794  phpar2  30814  phpar  30815  ipasslem5  30826  hvadd32  31025  hvaddsub12  31029  hvaddsubass  31032  hvsubass  31035  hvsub32  31036  hvsubdistr1  31040  hvsubdistr2  31041  hvmulcan  31063  hvmulcan2  31064  hvsubcan  31065  his5  31077  his2sub  31083  hhssabloilem  31252  hhssnv  31255  shlej2  31352  pjoi0  31708  hodcl  31738  hoadd32  31774  hosubdi  31799  hosubsub2  31803  hoaddsubass  31806  hosubsub4  31809  nmoplb  31898  unop  31906  hmop  31913  nmfnlb  31915  lnopmul  31958  kbass1  32107  kbass2  32108  leopmul2i  32126  leoptr  32128  cvntr  32283  mdslmd4i  32324  mdexchi  32326  atcv1  32371  sumdmdii  32406  fcoinvbr  32596  fpwrelmapffs  32728  xreceu  32913  isinftm  33161  unitdivcld  33925  esummulc1  34105  hasheuni  34109  unelsiga  34158  inelpisys  34178  carsgsigalem  34339  signswmnd  34581  bnj545  34918  bnj594  34935  bnj1311  35047  fissorduni  35112  r1filimi  35125  fineqvac  35150  fineqvnttrclselem3  35154  usgrgt2cycl  35185  subgrwlk  35187  acycgr1v  35204  cvmsf1o  35327  cvmscld  35328  satefvfmla1  35480  elnanelprv  35484  lediv2aALT  35732  gcd32  35804  fununiq  35824  dfrdg4  36006  brcolinear  36114  colinearex  36115  nn0prpwlem  36377  clsun  36383  fnemeet1  36421  fnemeet2  36422  fnejoin1  36423  fnejoin2  36424  eltail  36429  rdgeqoa  37425  nlpineqsn  37463  curf  37648  lindsadd  37663  poimirlem28  37698  cnambfre  37718  ftc1anclem4  37746  cocanfo  37769  f1ocan1fv  37776  metf1o  37805  ismtybnd  37857  ghomco  37941  isdrngo2  38008  inidl  38080  igenmin  38114  brxrn  38417  brredunds  38732  cmtvalN  39320  cvrval  39378  pmapmeet  39882  paddval  39907  paddssat  39923  elpcliN  40002  pclssN  40003  pclunN  40007  paddunN  40036  poldmj1N  40037  tendoplcl2  40887  tendoplcl  40890  dihmeet  41452  lcmineqlem1  42132  reltsub1  42494  reltsubadd2  42495  resubsub4  42497  reppncan  42501  resubdi  42504  readdcan2  42521  subresre  42539  mapco2g  42821  mzpcompact2lem  42858  eqrabdioph  42884  lerabdioph  42912  eluzrabdioph  42913  ltrabdioph  42915  nerabdioph  42916  dvdsrabdioph  42917  reglogcl  42997  rmxyadd  43028  rmyabs  43065  congadd  43073  congabseq  43081  rmydioph  43121  mendring  43295  mendlmod  43296  iocinico  43319  omge1  43404  relexp0a  43823  relexpaddss  43825  brcoffn  44137  ismnushort  44408  dvconstbi  44441  uzwo4  45164  ssin0  45166  ssinc  45198  ssdec  45199  fvmpt2bd  45281  disjf1o  45302  ssnnf1octb  45305  sub31  45405  fperiodmullem  45418  ssfiunibd  45424  infxr  45479  fmul01  45694  islptre  45733  lptre2pt  45752  limcleqr  45756  limclner  45763  limsuppnflem  45822  limsupvaluz2  45850  supcnvlimsup  45852  xlimmnfvlem2  45945  xlimmnfv  45946  xlimpnfvlem2  45949  xlimpnfv  45950  climxlim2lem  45957  coskpi2  45978  cosknegpi  45981  dvnmptdivc  46050  dvdsn1add  46051  dvnmptconst  46053  dvmptfprod  46057  dvnprodlem1  46058  dvnprodlem2  46059  ovolsplit  46100  stoweidlem60  46172  stowei  46176  dirkeritg  46214  fourierdlem70  46288  fourierdlem71  46289  fourierdlem103  46321  fourierdlem104  46322  fouriersw  46343  rrxtopnfi  46399  saluncl  46429  salexct  46446  sge0ltfirp  46512  sge0iunmpt  46530  meadjiunlem  46577  meaiuninc3v  46596  carageniuncllem1  46633  caratheodorylem1  46638  ovncvrrp  46676  ovnsubaddlem1  46682  hspmbllem2  46739  ovolval5lem3  46766  smfpimbor1lem1  46910  smfsuplem1  46923  smflimsuplem4  46935  sigarls  46969  cnambpcma  47408  elfzelfzlble  47435  submodaddmod  47455  difltmodne  47456  m1mod0mod1  47468  modmkpkne  47475  mod2addne  47478  modm2nep1  47480  modm1nep2  47482  modm1nem2  47483  fsumsplitsndif  47487  fundcmpsurinjALT  47526  iccpartiltu  47536  prproropf1olem2  47618  fmtno4prmfac  47686  2pwp1prmfmtno  47704  lighneallem4b  47723  mogoldbblem  47834  gbegt5  47875  sbgoldbm  47898  nnsum3primesle9  47908  nnsum4primesodd  47910  nnsum4primesoddALTV  47911  evengpoap3  47913  nnsum4primesevenALTV  47915  clnbgredg  47954  opstrgric  48040  clnbgrgrimlem  48047  grtrif1o  48056  isubgr3stgrlem1  48080  isubgr3stgrlem4  48083  gpgusgralem  48170  gpg3nbgrvtx0  48190  isupwlk  48250  lidldomnnring  48350  2zrngacmnd  48362  rhmsubcALTVlem2  48396  fprmappr  48459  zlmodzxzscm  48471  gsumlsscl  48494  lincvalsng  48531  lincvalpr  48533  lincdifsn  48539  linc1  48540  lincellss  48541  fdivmpt  48655  digexp  48722  2arymaptfo  48769  line  48847  rrxline  48849  itsclc0xyqsolr  48884  iscnrm3r  49062  resipos  49089  amgmwlem  49917