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  2628  spc3egv  3560  sbciegftOLD  3782  reuhyp  5362  predtrss  6274  onunel  6418  funopg  6520  funprg  6540  funtpg  6541  funcnvtp  6549  unima  6902  fvun1  6918  fnreseql  6986  xpprsng  7078  ftpg  7094  f1ounsn  7213  f13dfv  7215  f1ocoima  7244  f1ofvswap  7247  mpoeq3ia  7431  ordunel  7766  fex2  7876  funexw  7894  poxp  8068  poxp2  8083  poxp3  8090  poseq  8098  suppval1  8106  wfr3g  8259  smores3  8283  oaord  8472  oacan  8473  oaword  8474  omord  8493  omcan  8494  omwordri  8497  odi  8504  omass  8505  oeord  8513  oecan  8514  oewordri  8517  oeordsuc  8519  nnaord  8544  nnaordr  8545  nndi  8548  nnmass  8549  nnaword  8552  nnmord  8557  nnmwordri  8561  naddelim  8611  naddel1  8612  naddel2  8613  naddss1  8614  naddss2  8615  naddasslem2  8620  nadd32  8622  erov  8748  ecopovtrn  8754  ixpf  8854  f1oen4g  8897  f1dom4g  8898  mapxpen  9067  dif1enlemOLD  9081  ssfi  9097  sbthfilem  9122  sbthfi  9123  onomeneq  9138  fimax2g  9191  unbnn  9201  funisfsupp  9276  inelfi  9327  elfiun  9339  sup0  9376  suppr  9381  infpr  9414  ttrclss  9635  frr3g  9671  r111  9690  dif1card  9923  ackbij1lem16  10147  cff1  10171  cfflb  10172  cfsmolem  10183  fin23lem34  10259  hsmexlem2  10340  axcc3  10351  domtriomlem  10355  axdc3lem4  10366  axdc4lem  10368  axcclem  10370  konigthlem  10481  gchdomtri  10542  tskpr  10683  tskop  10684  tskuni  10696  tskun  10699  gruop  10718  gruun  10719  grudomon  10730  adderpqlem  10867  mulerpqlem  10868  addassnq  10871  mulassnq  10872  distrnq  10874  ltsonq  10882  ltanq  10884  ltmnq  10885  genpass  10922  distrlem1pr  10938  distrlem4pr  10939  ltsopr  10945  adddir  11125  axlttrn  11206  ltletr  11226  letr  11228  mul32  11300  mul31  11301  add32  11353  subsub23  11386  addsubass  11391  subcan2  11407  subsub2  11410  nppcan2  11413  sub32  11416  nnncan  11417  nnncan2  11419  pnpcan2  11422  subdi  11571  subdir  11572  receu  11783  mulcan1g  11791  mulcan2g  11792  divmul3  11802  divrec  11813  divrec2  11814  div11  11825  divsubdir  11836  subdivcomb2  11838  divdiv1  11853  redivcl  11861  div2neg  11865  ltmul2  11993  lemul1  11994  lemul2  11995  lemul2a  11997  lediv1  12008  gt0div  12009  ge0div  12010  mulsuble0b  12015  ltdivmul  12018  ledivmul  12019  ltdivmul2  12020  ledivmul2  12022  lemuldiv  12023  ltdiv23  12034  lediv23  12035  ledivp1i  12068  ltdivp1i  12069  uzind2  12587  nn0ind  12589  fnn0ind  12593  uz3m2nn  12813  xrltletr  13077  xrletr  13078  xrre2  13090  xrltmin  13102  xrlemin  13104  xleadd2a  13174  xleadd1  13175  xltadd2  13177  xmulasslem3  13206  xmulass  13207  xltmul2  13213  ixxdisj  13281  iooneg  13392  iccneg  13393  icoshft  13394  icoshftf1o  13395  icodisj  13397  snunioo  13399  fzen  13462  ssfzunsnext  13490  fzrev3  13511  2ffzeq  13570  fzoaddel2  13641  elfzodifsumelfzo  13652  ssfzoulel  13681  ssfzo12bi  13682  fzoopth  13683  fzoshftral  13705  adddivflid  13740  flltdivnn0lt  13755  ltdifltdiv  13756  fldiv4p1lem1div2  13757  modcyc  13828  modcyc2  13829  modaddabs  13833  muladdmod  13837  modsubmodmod  13855  modaddmodup  13859  modaddmulmod  13863  moddi  13864  modsubdir  13865  expdiv  14038  digit2  14161  nfile  14284  hashdifpr  14340  hashgt23el  14349  hashreshashfun  14364  hashf1dmcdm  14369  hash3tpexb  14419  fi1uzind  14432  ccatval1  14502  ccatass  14513  swrdval  14568  swrdnd  14579  swrd0  14583  swrdfv2  14586  pfxsuff1eqwrdeq  14623  swrdswrdlem  14628  pfxccatin12lem2a  14651  pfxccatin12lem1  14652  repswccat  14710  cshwidxmod  14727  cshwidxmodr  14728  cshf1  14734  repswcshw  14736  2cshw  14737  2cshwcom  14740  2cshwcshw  14750  cshwcsh2id  14753  ccatco  14760  2swrd2eqwrdeq  14878  wwlktovf  14881  brcnvtrclfv  14928  shftval2  15000  mulre  15046  absdiv  15220  absdiflt  15243  absdifle  15244  abs3dif  15257  cau3  15281  ello12r  15442  elo12r  15453  modfsummods  15718  geoisum1c  15805  rpnnen2lem4  16144  rpnnen2lem7  16147  addmulmodb  16194  dvdsmulc  16212  dvdsmulcr  16214  dvdsmultr1  16225  dvdsmultr2  16227  dvdssub2  16230  oexpneg  16274  divalgb  16333  ndvdsadd  16339  sadass  16400  modgcd  16461  dvdsgcd  16473  dvdsgcdb  16474  gcdass  16476  mulgcd  16477  absmulgcd  16478  rpmulgcd  16486  expgcd  16492  zexpgcd  16494  nn0seqcvgd  16499  algcvga  16508  lcmdvdsb  16542  lcmass  16543  lcmfunsnlem1  16566  lcmfunsnlem2lem1  16567  lcmfunsnlem2lem2  16568  coprmdvds  16582  coprmdvds2  16583  rpmul  16588  cncongr1  16596  cncongr2  16597  qnumdenbi  16673  modprm0  16735  coprimeprodsq  16738  pythagtriplem4  16749  pythagtriplem8  16753  pythagtriplem9  16754  pythagtriplem12  16756  pythagtriplem14  16758  pythagtriplem16  16760  pcpremul  16773  pcgcd  16808  vdwapval  16903  vdwapun  16904  prmgaplem3  16983  prmgaplem4  16984  prmgaplem7  16987  prmgapprmolem  16991  mreiincl  17516  mreincl  17519  mremre  17524  mrcss  17540  catcisolem  18035  pleval2  18259  pospo  18267  latlem  18361  latjcom  18371  latmcom  18387  lubss  18437  lubun  18439  clatglbss  18443  ipole  18458  ipolt  18459  pslem  18496  dirtr  18526  gsumsgrpccat  18732  gsumws2  18734  frmdmnd  18751  symggrplem  18776  isgrpi  18856  grpsubrcan  18918  grpinvsub  18919  grpsubeq0  18923  grpsubadd0sub  18924  grpnpcan  18929  qussub  19088  ghmsub  19121  symgpssefmnd  19293  symggrp  19297  symgextsymg  19321  gsmsymgreqlem2  19328  symgfixfolem1  19335  pmtrprfv3  19351  symggen  19367  lsmass  19566  efgsrel  19631  cntzcmn  19737  dvrcl  20307  unitdvcl  20308  dvrcan1  20312  subrngmre  20465  subrgmre  20500  rhmsubclem2  20589  rrgeq0  20603  abvsubtri  20730  abvtrivd  20735  lmodvsubval2  20838  rmodislmodlem  20850  rmodislmod  20851  lss0cl  20868  lssintcl  20885  lssincl  20886  reslmhm2  20975  lspvadd  21018  lspsntrim  21020  islbs3  21080  rnglidlmmgm  21170  cncrng  21313  cncrngOLD  21314  xrsmcmn  21316  cndrng  21323  cndrngOLD  21324  cnsrng  21330  absabv  21349  xrs1mnd  21365  psgnco  21508  zrhpsgninv  21510  zrhpsgnevpm  21516  zrhpsgnodpm  21517  zrhpsgnelbas  21519  zrhcopsgnelbas  21520  uvcresum  21718  lindfmm  21752  lindsmm  21753  evlsval2  22010  mamudm  22298  mamufacex  22299  matsubgcell  22337  matsc  22353  scmatscmide  22410  scmatrhmcl  22431  1marepvsma1  22486  m1detdiag  22500  mdetralt  22511  m2detleiblem7  22530  gsummatr01lem3  22560  gsummatr01  22562  smadiadetlem0  22564  decpmate  22669  decpmatcl  22670  pm2mpcl  22700  pm2mpghmlem2  22715  chfacfscmul0  22761  chfacfscmulgsum  22763  chfacfpmmul0  22765  chfacfpmmulgsum  22767  unopn  22806  clsss  22957  cldmre  22981  toponmre  22996  opnssneib  23018  restabs  23068  restcls  23084  restntr  23085  hausnei2  23256  cmpsublem  23302  bwth  23313  hausmapdom  23403  ptpjcn  23514  upxp  23526  ptrescn  23542  xkopjcn  23559  fbssfi  23740  snfil  23767  ufprim  23812  rnelfm  23856  flimrest  23886  fclsrest  23927  tmdgsum  23998  blpnfctr  24340  mscl  24365  xmscl  24366  xmsge0  24367  xmseq0  24368  restmetu  24474  ngpds  24508  tngngp3  24560  unitnmn0  24572  xrsxmet  24714  metds0  24755  mpomulcn  24774  cncfmptc  24821  isclmp  25013  cnlmod  25056  ncvsi  25067  cphsqrtcl  25100  cfil3i  25185  cfilres  25212  cmssmscld  25266  cmmbl  25451  voliunlem2  25468  itg2ub  25650  itgrecl  25715  r1pid  26082  eflogeq  26527  cxpadd  26604  cxpcom  26664  logbchbase  26697  relogbreexp  26701  relogbzexp  26702  relogbmulexp  26704  logbleb  26709  logblt  26710  lawcos  26742  pythag  26743  asinsinb  26823  acoscosb  26824  atantanb  26850  amgmlem  26916  lgsneg  27248  lgsne0  27262  lgsmodeq  27269  lgsmulsqcoprm  27270  gausslemma2dlem1a  27292  2sqreulem2  27379  sltres  27590  noetainflem1  27665  sltletr  27684  sletr  27686  nocvxmin  27707  madebdaylemold  27830  lrrecpo  27871  sltadd2im  27916  sleadd1im  27917  sleadd2im  27918  sleadd1  27919  sleadd2  27920  sltadd1  27922  addscan2  27923  addscan1  27924  subadds  27997  sltsub1  28003  divscl  28148  onscutlt  28188  zsoring  28319  expscllem  28340  0reno  28384  brbtwn2  28868  colinearalg  28873  eleesubd  28875  axcgrrflx  28877  axcgrtr  28878  axsegcon  28890  ax5seglem1  28891  ax5seglem2  28892  ax5seglem4  28895  axbtwnid  28902  axlowdimlem14  28918  axlowdim  28924  axcontlem5  28931  axcontlem7  28933  nb3grprlem2  29344  cplgr3v  29398  cusgrsizeindslem  29415  sizusglecusglem2  29426  umgr2v2e  29489  cusgrrusgr  29545  iswlk  29574  edginwlk  29598  uspgr2wlkeq  29609  uspgr2wlkeq2  29610  uspgr2wlkeqi  29611  wlkonprop  29620  wlkon2n0  29628  pthdadjvtx  29691  upgr2pthnlp  29695  spthonepeq  29715  pthdlem2lem  29730  crctcshwlkn0lem3  29775  crctcshwlkn0lem5  29777  wlkiswwlks2lem4  29835  wlkiswwlks2lem6  29837  wlklnwwlkln2lem  29845  wwlksnred  29855  wwlksnextbi  29857  wwlksnextwrd  29860  2pthdlem1  29893  2wlkdlem10  29898  umgr2adedgwlkonALT  29910  elwwlks2s3  29914  elwwlks2ons3im  29917  s3wwlks2on  29919  2wspdisj  29925  2wspiundisj  29926  clwwlkgt0  29948  clwlkclwwlklem2a4  29959  clwlkclwwlklem2a  29960  clwlkclwwlk  29964  clwlkclwwlk2  29965  clwlkclwwlkfo  29971  clwwisshclwwslemlem  29975  erclwwlktr  29984  clwwlkf  30009  wwlksubclwwlk  30020  erclwwlkntr  30033  clwwlknon  30052  frcond1  30228  frgr3v  30237  3vfriswmgr  30240  frgrwopreglem4a  30272  frrusgrord0lem  30301  clwwnonrepclwwnon  30307  extwwlkfab  30314  numclwwlk1lem2f1  30319  numclwwlk1lem2fo  30320  clwlknon2num  30330  numclwwlk2lem1  30338  numclwlk2lem2f  30339  numclwlk2lem2f1o  30341  numclwwlk2  30343  frgrreggt1  30355  friendshipgt3  30360  imsmetlem  30652  nmoxr  30728  nmoolb  30733  blometi  30765  phpar2  30785  phpar  30786  ipasslem5  30797  hvadd32  30996  hvaddsub12  31000  hvaddsubass  31003  hvsubass  31006  hvsub32  31007  hvsubdistr1  31011  hvsubdistr2  31012  hvmulcan  31034  hvmulcan2  31035  hvsubcan  31036  his5  31048  his2sub  31054  hhssabloilem  31223  hhssnv  31226  shlej2  31323  pjoi0  31679  hodcl  31709  hoadd32  31745  hosubdi  31770  hosubsub2  31774  hoaddsubass  31777  hosubsub4  31780  nmoplb  31869  unop  31877  hmop  31884  nmfnlb  31886  lnopmul  31929  kbass1  32078  kbass2  32079  leopmul2i  32097  leoptr  32099  cvntr  32254  mdslmd4i  32295  mdexchi  32297  atcv1  32342  sumdmdii  32377  fcoinvbr  32567  fpwrelmapffs  32690  xreceu  32875  isinftm  33136  unitdivcld  33870  esummulc1  34050  hasheuni  34054  unelsiga  34103  inelpisys  34123  carsgsigalem  34285  signswmnd  34527  bnj545  34864  bnj594  34881  bnj1311  34993  fineqvac  35074  usgrgt2cycl  35105  subgrwlk  35107  acycgr1v  35124  cvmsf1o  35247  cvmscld  35248  satefvfmla1  35400  elnanelprv  35404  lediv2aALT  35652  gcd32  35724  fununiq  35744  dfrdg4  35927  brcolinear  36035  colinearex  36036  nn0prpwlem  36298  clsun  36304  fnemeet1  36342  fnemeet2  36343  fnejoin1  36344  fnejoin2  36345  eltail  36350  rdgeqoa  37346  nlpineqsn  37384  curf  37580  lindsadd  37595  poimirlem28  37630  cnambfre  37650  ftc1anclem4  37678  cocanfo  37701  f1ocan1fv  37708  metf1o  37737  ismtybnd  37789  ghomco  37873  isdrngo2  37940  inidl  38012  igenmin  38046  brxrn  38344  brredunds  38605  cmtvalN  39192  cvrval  39250  pmapmeet  39755  paddval  39780  paddssat  39796  elpcliN  39875  pclssN  39876  pclunN  39880  paddunN  39909  poldmj1N  39910  tendoplcl2  40760  tendoplcl  40763  dihmeet  41325  lcmineqlem1  42005  reltsub1  42362  reltsubadd2  42363  resubsub4  42365  reppncan  42369  resubdi  42372  readdcan2  42389  subresre  42407  mapco2g  42690  mzpcompact2lem  42727  eqrabdioph  42753  lerabdioph  42781  eluzrabdioph  42782  ltrabdioph  42784  nerabdioph  42785  dvdsrabdioph  42786  reglogcl  42866  rmxyadd  42897  rmyabs  42934  congadd  42942  congabseq  42950  rmydioph  42990  mendring  43164  mendlmod  43165  iocinico  43188  omge1  43273  relexp0a  43692  relexpaddss  43694  brcoffn  44006  ismnushort  44277  dvconstbi  44310  uzwo4  45034  ssin0  45036  ssinc  45068  ssdec  45069  fvmpt2bd  45151  disjf1o  45172  ssnnf1octb  45175  sub31  45275  fperiodmullem  45288  ssfiunibd  45294  infxr  45350  fmul01  45565  islptre  45604  lptre2pt  45625  limcleqr  45629  limclner  45636  limsuppnflem  45695  limsupvaluz2  45723  supcnvlimsup  45725  xlimmnfvlem2  45818  xlimmnfv  45819  xlimpnfvlem2  45822  xlimpnfv  45823  climxlim2lem  45830  coskpi2  45851  cosknegpi  45854  dvnmptdivc  45923  dvdsn1add  45924  dvnmptconst  45926  dvmptfprod  45930  dvnprodlem1  45931  dvnprodlem2  45932  ovolsplit  45973  stoweidlem60  46045  stowei  46049  dirkeritg  46087  fourierdlem70  46161  fourierdlem71  46162  fourierdlem103  46194  fourierdlem104  46195  fouriersw  46216  rrxtopnfi  46272  saluncl  46302  salexct  46319  sge0ltfirp  46385  sge0iunmpt  46403  meadjiunlem  46450  meaiuninc3v  46469  carageniuncllem1  46506  caratheodorylem1  46511  ovncvrrp  46549  ovnsubaddlem1  46555  hspmbllem2  46612  ovolval5lem3  46639  smfpimbor1lem1  46783  smfsuplem1  46796  smflimsuplem4  46808  sigarls  46842  cnambpcma  47282  elfzelfzlble  47309  submodaddmod  47329  difltmodne  47330  m1mod0mod1  47342  modmkpkne  47349  mod2addne  47352  modm2nep1  47354  modm1nep2  47356  modm1nem2  47357  fsumsplitsndif  47361  fundcmpsurinjALT  47400  iccpartiltu  47410  prproropf1olem2  47492  fmtno4prmfac  47560  2pwp1prmfmtno  47578  lighneallem4b  47597  mogoldbblem  47708  gbegt5  47749  sbgoldbm  47772  nnsum3primesle9  47782  nnsum4primesodd  47784  nnsum4primesoddALTV  47785  evengpoap3  47787  nnsum4primesevenALTV  47789  clnbgredg  47828  opstrgric  47914  clnbgrgrimlem  47921  grtrif1o  47930  isubgr3stgrlem1  47954  isubgr3stgrlem4  47957  gpgusgralem  48044  gpg3nbgrvtx0  48064  isupwlk  48124  lidldomnnring  48224  2zrngacmnd  48236  rhmsubcALTVlem2  48270  fprmappr  48333  zlmodzxzscm  48345  gsumlsscl  48368  lincvalsng  48405  lincvalpr  48407  lincdifsn  48413  linc1  48414  lincellss  48415  fdivmpt  48529  digexp  48596  2arymaptfo  48643  line  48721  rrxline  48723  itsclc0xyqsolr  48758  iscnrm3r  48936  resipos  48963  amgmwlem  49791