Theorem 3adant1 1131

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  3ad2ant2  1135  3ad2ant3  1136  3simpc  1151  eupickb  2635  spc3egv  3545  sbciegftOLD  3766  reuhyp  5362  predtrss  6286  onunel  6430  funopg  6532  funprg  6552  funtpg  6553  funcnvtp  6561  unima  6915  fvun1  6931  fnreseql  7000  xpprsng  7093  ftpg  7110  f1ounsn  7227  f13dfv  7229  f1ocoima  7258  f1ofvswap  7261  mpoeq3ia  7445  ordunel  7778  fex2  7887  funexw  7905  poxp  8078  poxp2  8093  poxp3  8100  poseq  8108  suppval1  8116  wfr3g  8269  smores3  8293  oaord  8482  oacan  8483  oaword  8484  omord  8503  omcan  8504  omwordri  8507  odi  8514  omass  8515  oeord  8524  oecan  8525  oewordri  8528  oeordsuc  8530  nnaord  8555  nnaordr  8556  nndi  8559  nnmass  8560  nnaword  8563  nnmord  8568  nnmwordri  8572  naddelim  8622  naddel1  8623  naddel2  8624  naddss1  8625  naddss2  8626  naddasslem2  8631  nadd32  8633  erov  8761  ecopovtrn  8767  ixpf  8868  f1oen4g  8911  f1dom4g  8912  mapxpen  9081  ssfi  9107  sbthfilem  9132  sbthfi  9133  onomeneq  9148  fimax2g  9196  unbnn  9206  funisfsupp  9280  inelfi  9331  elfiun  9343  sup0  9380  suppr  9385  infpr  9418  ttrclss  9641  frr3g  9680  r111  9699  dif1card  9932  ackbij1lem16  10156  cff1  10180  cfflb  10181  cfsmolem  10192  fin23lem34  10268  hsmexlem2  10349  axcc3  10360  domtriomlem  10364  axdc3lem4  10375  axdc4lem  10377  axcclem  10379  konigthlem  10491  gchdomtri  10552  tskpr  10693  tskop  10694  tskuni  10706  tskun  10709  gruop  10728  gruun  10729  grudomon  10740  adderpqlem  10877  mulerpqlem  10878  addassnq  10881  mulassnq  10882  distrnq  10884  ltsonq  10892  ltanq  10894  ltmnq  10895  genpass  10932  distrlem1pr  10948  distrlem4pr  10949  ltsopr  10955  adddir  11135  axlttrn  11218  ltletr  11238  letr  11240  mul32  11312  mul31  11313  add32  11365  subsub23  11398  addsubass  11403  subcan2  11419  subsub2  11422  nppcan2  11425  sub32  11428  nnncan  11429  nnncan2  11431  pnpcan2  11434  subdi  11583  subdir  11584  receu  11795  mulcan1g  11803  mulcan2g  11804  divmul3  11814  divrec  11825  divrec2  11826  div11  11837  divsubdir  11848  subdivcomb2  11851  divdiv1  11866  redivcl  11874  div2neg  11878  ltmul2  12006  lemul1  12007  lemul2  12008  lemul2a  12010  lediv1  12021  gt0div  12022  ge0div  12023  mulsuble0b  12028  ltdivmul  12031  ledivmul  12032  ltdivmul2  12033  ledivmul2  12035  lemuldiv  12036  ltdiv23  12047  lediv23  12048  ledivp1i  12081  ltdivp1i  12082  uzind2  12622  nn0ind  12624  fnn0ind  12628  uz3m2nn  12844  xrltletr  13108  xrletr  13109  xrre2  13122  xrltmin  13134  xrlemin  13136  xleadd2a  13206  xleadd1  13207  xltadd2  13209  xmulasslem3  13238  xmulass  13239  xltmul2  13245  ixxdisj  13313  iooneg  13424  iccneg  13425  icoshft  13426  icoshftf1o  13427  icodisj  13429  snunioo  13431  fzen  13495  ssfzunsnext  13523  fzrev3  13544  2ffzeq  13603  fzoaddel2  13675  elfzodifsumelfzo  13686  ssfzoulel  13715  ssfzo12bi  13716  fzoopth  13717  fzoshftral  13742  adddivflid  13777  flltdivnn0lt  13792  ltdifltdiv  13793  fldiv4p1lem1div2  13794  modcyc  13865  modcyc2  13866  modaddabs  13870  muladdmod  13874  modsubmodmod  13892  modaddmodup  13896  modaddmulmod  13900  moddi  13901  modsubdir  13902  expdiv  14075  digit2  14198  nfile  14321  hashdifpr  14377  hashgt23el  14386  hashreshashfun  14401  hashf1dmcdm  14406  hash3tpexb  14456  fi1uzind  14469  ccatval1  14539  ccatass  14551  swrdval  14606  swrdnd  14617  swrd0  14621  swrdfv2  14624  pfxsuff1eqwrdeq  14661  swrdswrdlem  14666  pfxccatin12lem2a  14689  pfxccatin12lem1  14690  repswccat  14748  cshwidxmod  14765  cshwidxmodr  14766  cshf1  14772  repswcshw  14774  2cshw  14775  2cshwcom  14778  2cshwcshw  14787  cshwcsh2id  14790  ccatco  14797  2swrd2eqwrdeq  14915  wwlktovf  14918  brcnvtrclfv  14965  shftval2  15037  mulre  15083  absdiv  15257  absdiflt  15280  absdifle  15281  abs3dif  15294  cau3  15318  ello12r  15479  elo12r  15490  modfsummods  15756  geoisum1c  15845  rpnnen2lem4  16184  rpnnen2lem7  16187  addmulmodb  16234  dvdsmulc  16252  dvdsmulcr  16254  dvdsmultr1  16265  dvdsmultr2  16267  dvdssub2  16270  oexpneg  16314  divalgb  16373  ndvdsadd  16379  sadass  16440  modgcd  16501  dvdsgcd  16513  dvdsgcdb  16514  gcdass  16516  mulgcd  16517  absmulgcd  16518  rpmulgcd  16526  expgcd  16532  zexpgcd  16534  nn0seqcvgd  16539  algcvga  16548  lcmdvdsb  16582  lcmass  16583  lcmfunsnlem1  16606  lcmfunsnlem2lem1  16607  lcmfunsnlem2lem2  16608  coprmdvds  16622  coprmdvds2  16623  rpmul  16628  cncongr1  16636  cncongr2  16637  qnumdenbi  16714  modprm0  16776  coprimeprodsq  16779  pythagtriplem4  16790  pythagtriplem8  16794  pythagtriplem9  16795  pythagtriplem12  16797  pythagtriplem14  16799  pythagtriplem16  16801  pcpremul  16814  pcgcd  16849  vdwapval  16944  vdwapun  16945  prmgaplem3  17024  prmgaplem4  17025  prmgaplem7  17028  prmgapprmolem  17032  mreiincl  17558  mreincl  17561  mremre  17566  mrcss  17582  catcisolem  18077  pleval2  18301  pospo  18309  latlem  18403  latjcom  18413  latmcom  18429  lubss  18479  lubun  18481  clatglbss  18485  ipole  18500  ipolt  18501  pslem  18538  dirtr  18568  gsumsgrpccat  18808  gsumws2  18810  frmdmnd  18827  symggrplem  18852  isgrpi  18935  grpsubrcan  18997  grpinvsub  18998  grpsubeq0  19002  grpsubadd0sub  19003  grpnpcan  19008  qussub  19166  ghmsub  19199  symgpssefmnd  19371  symggrp  19375  symgextsymg  19399  gsmsymgreqlem2  19406  symgfixfolem1  19413  pmtrprfv3  19429  symggen  19445  lsmass  19644  efgsrel  19709  cntzcmn  19815  dvrcl  20384  unitdvcl  20385  dvrcan1  20389  subrngmre  20539  subrgmre  20574  rhmsubclem2  20663  rrgeq0  20677  abvsubtri  20804  abvtrivd  20809  lmodvsubval2  20912  rmodislmodlem  20924  rmodislmod  20925  lss0cl  20942  lssintcl  20959  lssincl  20960  reslmhm2  21048  lspvadd  21091  lspsntrim  21093  islbs3  21153  rnglidlmmgm  21243  cncrng  21373  xrsmcmn  21375  cndrng  21381  cnsrng  21386  absabv  21404  xrs1mnd  21420  psgnco  21563  zrhpsgninv  21565  zrhpsgnevpm  21571  zrhpsgnodpm  21572  zrhpsgnelbas  21574  zrhcopsgnelbas  21575  uvcresum  21773  lindfmm  21807  lindsmm  21808  evlsval2  22065  mamudm  22360  mamufacex  22361  matsubgcell  22399  matsc  22415  scmatscmide  22472  scmatrhmcl  22493  1marepvsma1  22548  m1detdiag  22562  mdetralt  22573  m2detleiblem7  22592  gsummatr01lem3  22622  gsummatr01  22624  smadiadetlem0  22626  decpmate  22731  decpmatcl  22732  pm2mpcl  22762  pm2mpghmlem2  22777  chfacfscmul0  22823  chfacfscmulgsum  22825  chfacfpmmul0  22827  chfacfpmmulgsum  22829  unopn  22868  clsss  23019  cldmre  23043  toponmre  23058  opnssneib  23080  restabs  23130  restcls  23146  restntr  23147  hausnei2  23318  cmpsublem  23364  bwth  23375  hausmapdom  23465  ptpjcn  23576  upxp  23588  ptrescn  23604  xkopjcn  23621  fbssfi  23802  snfil  23829  ufprim  23874  rnelfm  23918  flimrest  23948  fclsrest  23989  tmdgsum  24060  blpnfctr  24401  mscl  24426  xmscl  24427  xmsge0  24428  xmseq0  24429  restmetu  24535  ngpds  24569  tngngp3  24621  unitnmn0  24633  xrsxmet  24775  metds0  24816  mpomulcn  24834  cncfmptc  24879  isclmp  25064  cnlmod  25107  ncvsi  25118  cphsqrtcl  25151  cfil3i  25236  cfilres  25263  cmssmscld  25317  cmmbl  25501  voliunlem2  25518  itg2ub  25700  itgrecl  25765  r1pid  26126  eflogeq  26566  cxpadd  26643  cxpcom  26703  logbchbase  26735  relogbreexp  26739  relogbzexp  26740  relogbmulexp  26742  logbleb  26747  logblt  26748  lawcos  26780  pythag  26781  asinsinb  26861  acoscosb  26862  atantanb  26888  amgmlem  26953  lgsneg  27284  lgsne0  27298  lgsmodeq  27305  lgsmulsqcoprm  27306  gausslemma2dlem1a  27328  2sqreulem2  27415  ltsres  27626  noetainflem1  27701  ltlestr  27724  lestr  27726  nocvxmin  27747  madebdaylemold  27890  lrrecpo  27933  ltadds2im  27978  leadds1im  27979  leadds2im  27980  leadds1  27981  leadds2  27982  ltadds1  27984  addscan2  27985  addscan1  27986  subadds  28062  ltsubs1  28068  divscl  28215  oncutlt  28256  zsoring  28401  expscllem  28422  brbtwn2  28974  colinearalg  28979  eleesubd  28981  axcgrrflx  28983  axcgrtr  28984  axsegcon  28996  ax5seglem1  28997  ax5seglem2  28998  ax5seglem4  29001  axbtwnid  29008  axlowdimlem14  29024  axlowdim  29030  axcontlem5  29037  axcontlem7  29039  nb3grprlem2  29450  cplgr3v  29504  cusgrsizeindslem  29520  sizusglecusglem2  29531  umgr2v2e  29594  cusgrrusgr  29650  iswlk  29679  edginwlk  29703  uspgr2wlkeq  29714  uspgr2wlkeq2  29715  uspgr2wlkeqi  29716  wlkonprop  29725  wlkon2n0  29733  pthdadjvtx  29796  upgr2pthnlp  29800  spthonepeq  29820  pthdlem2lem  29835  crctcshwlkn0lem3  29880  crctcshwlkn0lem5  29882  wlkiswwlks2lem4  29940  wlkiswwlks2lem6  29942  wlklnwwlkln2lem  29950  wwlksnred  29960  wwlksnextbi  29962  wwlksnextwrd  29965  2pthdlem1  29998  2wlkdlem10  30003  umgr2adedgwlkonALT  30015  elwwlks2s3  30019  elwwlks2ons3im  30022  s3wwlks2on  30024  sps3wwlks2on  30025  2wspdisj  30033  2wspiundisj  30034  clwwlkgt0  30056  clwlkclwwlklem2a4  30067  clwlkclwwlklem2a  30068  clwlkclwwlk  30072  clwlkclwwlk2  30073  clwlkclwwlkfo  30079  clwwisshclwwslemlem  30083  erclwwlktr  30092  clwwlkf  30117  wwlksubclwwlk  30128  erclwwlkntr  30141  clwwlknon  30160  frcond1  30336  frgr3v  30345  3vfriswmgr  30348  frgrwopreglem4a  30380  frrusgrord0lem  30409  clwwnonrepclwwnon  30415  extwwlkfab  30422  numclwwlk1lem2f1  30427  numclwwlk1lem2fo  30428  clwlknon2num  30438  numclwwlk2lem1  30446  numclwlk2lem2f  30447  numclwlk2lem2f1o  30449  numclwwlk2  30451  frgrreggt1  30463  friendshipgt3  30468  imsmetlem  30761  nmoxr  30837  nmoolb  30842  blometi  30874  phpar2  30894  phpar  30895  ipasslem5  30906  hvadd32  31105  hvaddsub12  31109  hvaddsubass  31112  hvsubass  31115  hvsub32  31116  hvsubdistr1  31120  hvsubdistr2  31121  hvmulcan  31143  hvmulcan2  31144  hvsubcan  31145  his5  31157  his2sub  31163  hhssabloilem  31332  hhssnv  31335  shlej2  31432  pjoi0  31788  hodcl  31818  hoadd32  31854  hosubdi  31879  hosubsub2  31883  hoaddsubass  31886  hosubsub4  31889  nmoplb  31978  unop  31986  hmop  31993  nmfnlb  31995  lnopmul  32038  kbass1  32187  kbass2  32188  leopmul2i  32206  leoptr  32208  cvntr  32363  mdslmd4i  32404  mdexchi  32406  atcv1  32451  sumdmdii  32486  fcoinvbr  32675  fpwrelmapffs  32807  xreceu  32981  isinftm  33242  unitdivcld  34045  esummulc1  34225  hasheuni  34229  unelsiga  34278  inelpisys  34298  carsgsigalem  34459  signswmnd  34701  bnj545  35037  bnj594  35054  bnj1311  35166  fissorduni  35233  r1filimi  35246  fineqvac  35260  fineqvnttrclselem3  35267  fineqvinfep  35269  usgrgt2cycl  35312  subgrwlk  35314  acycgr1v  35331  cvmsf1o  35454  cvmscld  35455  satefvfmla1  35607  elnanelprv  35611  lediv2aALT  35859  gcd32  35931  fununiq  35951  dfrdg4  36133  brcolinear  36241  colinearex  36242  nn0prpwlem  36504  clsun  36510  fnemeet1  36548  fnemeet2  36549  fnejoin1  36550  fnejoin2  36551  eltail  36556  rdgeqoa  37686  nlpineqsn  37724  curf  37919  lindsadd  37934  poimirlem28  37969  cnambfre  37989  ftc1anclem4  38017  cocanfo  38040  f1ocan1fv  38047  metf1o  38076  ismtybnd  38128  ghomco  38212  isdrngo2  38279  inidl  38351  igenmin  38385  brxrn  38704  brredunds  39031  cmtvalN  39657  cvrval  39715  pmapmeet  40219  paddval  40244  paddssat  40260  elpcliN  40339  pclssN  40340  pclunN  40344  paddunN  40373  poldmj1N  40374  tendoplcl2  41224  tendoplcl  41227  dihmeet  41789  lcmineqlem1  42468  reltsub1  42818  reltsubadd2  42819  resubsub4  42821  reppncan  42825  resubdi  42828  readdcan2  42845  subresre  42863  mapco2g  43146  mzpcompact2lem  43183  eqrabdioph  43209  lerabdioph  43233  eluzrabdioph  43234  ltrabdioph  43236  nerabdioph  43237  dvdsrabdioph  43238  reglogcl  43318  rmxyadd  43349  rmyabs  43386  congadd  43394  congabseq  43402  rmydioph  43442  mendring  43616  mendlmod  43617  iocinico  43640  omge1  43725  relexp0a  44143  relexpaddss  44145  brcoffn  44457  ismnushort  44728  dvconstbi  44761  uzwo4  45484  ssin0  45486  ssinc  45517  ssdec  45518  fvmpt2bd  45600  disjf1o  45621  ssnnf1octb  45624  sub31  45723  fperiodmullem  45736  ssfiunibd  45742  infxr  45796  fmul01  46010  islptre  46049  lptre2pt  46068  limcleqr  46072  limclner  46079  limsuppnflem  46138  limsupvaluz2  46166  supcnvlimsup  46168  xlimmnfvlem2  46261  xlimmnfv  46262  xlimpnfvlem2  46265  xlimpnfv  46266  climxlim2lem  46273  coskpi2  46294  cosknegpi  46297  dvnmptdivc  46366  dvdsn1add  46367  dvnmptconst  46369  dvmptfprod  46373  dvnprodlem1  46374  dvnprodlem2  46375  ovolsplit  46416  stoweidlem60  46488  stowei  46492  dirkeritg  46530  fourierdlem70  46604  fourierdlem71  46605  fourierdlem103  46637  fourierdlem104  46638  fouriersw  46659  rrxtopnfi  46715  saluncl  46745  salexct  46762  sge0ltfirp  46828  sge0iunmpt  46846  meadjiunlem  46893  meaiuninc3v  46912  carageniuncllem1  46949  caratheodorylem1  46954  ovncvrrp  46992  ovnsubaddlem1  46998  hspmbllem2  47055  ovolval5lem3  47082  smfpimbor1lem1  47226  smfsuplem1  47239  smflimsuplem4  47251  sigarls  47285  cnambpcma  47742  elfzelfzlble  47769  submodaddmod  47795  difltmodne  47796  m1mod0mod1  47808  modmkpkne  47815  mod2addne  47818  modm2nep1  47820  modm1nep2  47822  modm1nem2  47823  fsumsplitsndif  47829  fundcmpsurinjALT  47872  iccpartiltu  47882  prproropf1olem2  47964  fmtno4prmfac  48035  2pwp1prmfmtno  48053  lighneallem4b  48072  nprmdvdsfacm1lem4  48086  mogoldbblem  48196  gbegt5  48237  sbgoldbm  48260  nnsum3primesle9  48270  nnsum4primesodd  48272  nnsum4primesoddALTV  48273  evengpoap3  48275  nnsum4primesevenALTV  48277  clnbgredg  48316  opstrgric  48402  clnbgrgrimlem  48409  grtrif1o  48418  isubgr3stgrlem1  48442  isubgr3stgrlem4  48445  gpgusgralem  48532  gpg3nbgrvtx0  48552  isupwlk  48612  lidldomnnring  48712  2zrngacmnd  48724  rhmsubcALTVlem2  48758  fprmappr  48821  zlmodzxzscm  48833  gsumlsscl  48856  lincvalsng  48892  lincvalpr  48894  lincdifsn  48900  linc1  48901  lincellss  48902  fdivmpt  49016  digexp  49083  2arymaptfo  49130  line  49208  rrxline  49210  itsclc0xyqsolr  49245  iscnrm3r  49423  resipos  49450  amgmwlem  50277