Theorem 3adant1 1129

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  1133  3ad2ant3  1134  3simpc  1149  eupickb  2632  spc3egv  3602  sbciegftOLD  3829  reuhyp  5425  predtrss  6344  onunel  6490  funopg  6601  funprg  6621  funtpg  6622  funcnvtp  6630  unima  6983  fvun1  6999  fnreseql  7067  xpprsng  7159  ftpg  7175  f1ounsn  7291  f13dfv  7293  f1ocoima  7322  f1ofvswap  7325  mpoeq3ia  7510  ordunel  7846  fex2  7956  funexw  7974  poxp  8151  poxp2  8166  poxp3  8173  poseq  8181  suppval1  8189  wfr3g  8345  smores3  8391  oaord  8583  oacan  8584  oaword  8585  omord  8604  omcan  8605  omwordri  8608  odi  8615  omass  8616  oeord  8624  oecan  8625  oewordri  8628  oeordsuc  8630  nnaord  8655  nnaordr  8656  nndi  8659  nnmass  8660  nnaword  8663  nnmord  8668  nnmwordri  8672  naddelim  8722  naddel1  8723  naddel2  8724  naddss1  8725  naddss2  8726  naddasslem2  8731  nadd32  8733  erov  8852  ecopovtrn  8858  ixpf  8958  f1oen4g  9003  f1dom4g  9004  mapxpen  9181  dif1enlemOLD  9195  ssfi  9211  sbthfilem  9235  sbthfi  9236  onomeneq  9262  fimax2g  9319  unbnn  9329  funisfsupp  9404  inelfi  9455  elfiun  9467  sup0  9503  suppr  9508  infpr  9540  ttrclss  9757  frr3g  9793  r111  9812  dif1card  10047  ackbij1lem16  10271  cff1  10295  cfflb  10296  cfsmolem  10307  fin23lem34  10383  hsmexlem2  10464  axcc3  10475  domtriomlem  10479  axdc3lem4  10490  axdc4lem  10492  axcclem  10494  konigthlem  10605  gchdomtri  10666  tskpr  10807  tskop  10808  tskuni  10820  tskun  10823  gruop  10842  gruun  10843  grudomon  10854  adderpqlem  10991  mulerpqlem  10992  addassnq  10995  mulassnq  10996  distrnq  10998  ltsonq  11006  ltanq  11008  ltmnq  11009  genpass  11046  distrlem1pr  11062  distrlem4pr  11063  ltsopr  11069  adddir  11249  axlttrn  11330  ltletr  11350  letr  11352  mul32  11424  mul31  11425  add32  11477  subsub23  11510  addsubass  11515  subcan2  11531  subsub2  11534  nppcan2  11537  sub32  11540  nnncan  11541  nnncan2  11543  pnpcan2  11546  subdi  11693  subdir  11694  receu  11905  mulcan1g  11913  mulcan2g  11914  divmul3  11924  divrec  11935  divrec2  11936  div11  11947  divsubdir  11958  subdivcomb2  11960  divdiv1  11975  redivcl  11983  div2neg  11987  ltmul2  12115  lemul1  12116  lemul2  12117  lemul2a  12119  lediv1  12130  gt0div  12131  ge0div  12132  mulsuble0b  12137  ltdivmul  12140  ledivmul  12141  ltdivmul2  12142  ledivmul2  12144  lemuldiv  12145  ltdiv23  12156  lediv23  12157  ledivp1i  12190  ltdivp1i  12191  uzind2  12708  nn0ind  12710  fnn0ind  12714  uz3m2nn  12930  xrltletr  13195  xrletr  13196  xrre2  13208  xrltmin  13220  xrlemin  13222  xleadd2a  13292  xleadd1  13293  xltadd2  13295  xmulasslem3  13324  xmulass  13325  xltmul2  13331  ixxdisj  13398  iooneg  13507  iccneg  13508  icoshft  13509  icoshftf1o  13510  icodisj  13512  snunioo  13514  fzen  13577  ssfzunsnext  13605  fzrev3  13626  2ffzeq  13685  fzoaddel2  13755  elfzodifsumelfzo  13766  ssfzoulel  13795  ssfzo12bi  13796  fzoopth  13797  fzoshftral  13819  adddivflid  13854  flltdivnn0lt  13869  ltdifltdiv  13870  fldiv4p1lem1div2  13871  modcyc  13942  modcyc2  13943  modaddabs  13945  muladdmod  13949  modsubmodmod  13967  modaddmodup  13971  modaddmulmod  13975  moddi  13976  modsubdir  13977  expdiv  14150  digit2  14271  nfile  14394  hashdifpr  14450  hashgt23el  14459  hashreshashfun  14474  hashf1dmcdm  14479  hash3tpexb  14529  fi1uzind  14542  ccatval1  14611  ccatass  14622  swrdval  14677  swrdnd  14688  swrd0  14692  swrdfv2  14695  pfxsuff1eqwrdeq  14733  swrdswrdlem  14738  pfxccatin12lem2a  14761  pfxccatin12lem1  14762  repswccat  14820  cshwidxmod  14837  cshwidxmodr  14838  cshf1  14844  repswcshw  14846  2cshw  14847  2cshwcom  14850  2cshwcshw  14860  cshwcsh2id  14863  ccatco  14870  2swrd2eqwrdeq  14988  wwlktovf  14991  brcnvtrclfv  15038  shftval2  15110  mulre  15156  absdiv  15330  absdiflt  15352  absdifle  15353  abs3dif  15366  cau3  15390  ello12r  15549  elo12r  15560  modfsummods  15825  geoisum1c  15912  rpnnen2lem4  16249  rpnnen2lem7  16252  addmulmodb  16299  dvdsmulc  16317  dvdsmulcr  16319  dvdsmultr1  16329  dvdsmultr2  16331  dvdssub2  16334  oexpneg  16378  divalgb  16437  ndvdsadd  16443  sadass  16504  modgcd  16565  dvdsgcd  16577  dvdsgcdb  16578  gcdass  16580  mulgcd  16581  absmulgcd  16582  rpmulgcd  16590  expgcd  16596  zexpgcd  16598  nn0seqcvgd  16603  algcvga  16612  lcmdvdsb  16646  lcmass  16647  lcmfunsnlem1  16670  lcmfunsnlem2lem1  16671  lcmfunsnlem2lem2  16672  coprmdvds  16686  coprmdvds2  16687  rpmul  16692  cncongr1  16700  cncongr2  16701  qnumdenbi  16777  modprm0  16838  coprimeprodsq  16841  pythagtriplem4  16852  pythagtriplem8  16856  pythagtriplem9  16857  pythagtriplem12  16859  pythagtriplem14  16861  pythagtriplem16  16863  pcpremul  16876  pcgcd  16911  vdwapval  17006  vdwapun  17007  prmgaplem3  17086  prmgaplem4  17087  prmgaplem7  17090  prmgapprmolem  17094  mreiincl  17640  mreincl  17643  mremre  17648  mrcss  17660  catcisolem  18163  pleval2  18394  pospo  18402  latlem  18494  latjcom  18504  latmcom  18520  lubss  18570  lubun  18572  clatglbss  18576  ipole  18591  ipolt  18592  pslem  18629  dirtr  18659  gsumsgrpccat  18865  gsumws2  18867  frmdmnd  18884  symggrplem  18909  isgrpi  18989  grpsubrcan  19051  grpinvsub  19052  grpsubeq0  19056  grpsubadd0sub  19057  grpnpcan  19062  qussub  19221  ghmsub  19254  symgpssefmnd  19427  symggrp  19432  symgextsymg  19456  gsmsymgreqlem2  19463  symgfixfolem1  19470  pmtrprfv3  19486  symggen  19502  lsmass  19701  efgsrel  19766  cntzcmn  19872  dvrcl  20420  unitdvcl  20421  dvrcan1  20425  subrngmre  20578  subrgmre  20613  rhmsubclem2  20702  rrgeq0  20716  abvsubtri  20844  abvtrivd  20849  lmodvsubval2  20931  rmodislmodlem  20943  rmodislmod  20944  rmodislmodOLD  20945  lss0cl  20962  lssintcl  20979  lssincl  20980  reslmhm2  21069  lspvadd  21112  lspsntrim  21114  islbs3  21174  rnglidlmmgm  21272  cncrng  21418  cncrngOLD  21419  xrsmcmn  21421  cndrng  21428  cndrngOLD  21429  cnsrng  21435  xrs1mnd  21439  absabv  21459  psgnco  21618  zrhpsgninv  21620  zrhpsgnevpm  21626  zrhpsgnodpm  21627  zrhpsgnelbas  21629  zrhcopsgnelbas  21630  uvcresum  21830  lindfmm  21864  lindsmm  21865  evlsval2  22128  mamudm  22414  mamufacex  22415  matsubgcell  22455  matsc  22471  scmatscmide  22528  scmatrhmcl  22549  1marepvsma1  22604  m1detdiag  22618  mdetralt  22629  m2detleiblem7  22648  gsummatr01lem3  22678  gsummatr01  22680  smadiadetlem0  22682  decpmate  22787  decpmatcl  22788  pm2mpcl  22818  pm2mpghmlem2  22833  chfacfscmul0  22879  chfacfscmulgsum  22881  chfacfpmmul0  22883  chfacfpmmulgsum  22885  unopn  22924  clsss  23077  cldmre  23101  toponmre  23116  opnssneib  23138  restabs  23188  restcls  23204  restntr  23205  hausnei2  23376  cmpsublem  23422  bwth  23433  hausmapdom  23523  ptpjcn  23634  upxp  23646  ptrescn  23662  xkopjcn  23679  fbssfi  23860  snfil  23887  ufprim  23932  rnelfm  23976  flimrest  24006  fclsrest  24047  tmdgsum  24118  blpnfctr  24461  mscl  24486  xmscl  24487  xmsge0  24488  xmseq0  24489  restmetu  24598  ngpds  24632  tngngp3  24692  unitnmn0  24704  xrsxmet  24844  metds0  24885  mpomulcn  24904  cncfmptc  24951  isclmp  25143  cnlmod  25186  ncvsi  25198  cphsqrtcl  25231  cfil3i  25316  cfilres  25343  cmssmscld  25397  cmmbl  25582  voliunlem2  25599  itg2ub  25782  itgrecl  25847  r1pid  26214  eflogeq  26658  cxpadd  26735  cxpcom  26795  logbchbase  26828  relogbreexp  26832  relogbzexp  26833  relogbmulexp  26835  logbleb  26840  logblt  26841  lawcos  26873  pythag  26874  asinsinb  26954  acoscosb  26955  atantanb  26981  amgmlem  27047  lgsneg  27379  lgsne0  27393  lgsmodeq  27400  lgsmulsqcoprm  27401  gausslemma2dlem1a  27423  2sqreulem2  27510  sltres  27721  noetainflem1  27796  sltletr  27815  sletr  27817  nocvxmin  27837  madebdaylemold  27950  lrrecpo  27988  sltadd2im  28033  sleadd1im  28034  sleadd2im  28035  sleadd1  28036  sleadd2  28037  sltadd1  28039  addscan2  28040  addscan1  28041  subadds  28114  sltsub1  28120  divscl  28261  nohalf  28421  0reno  28443  brbtwn2  28934  colinearalg  28939  eleesubd  28941  axcgrrflx  28943  axcgrtr  28944  axsegcon  28956  ax5seglem1  28957  ax5seglem2  28958  ax5seglem4  28961  axbtwnid  28968  axlowdimlem14  28984  axlowdim  28990  axcontlem5  28997  axcontlem7  28999  nb3grprlem2  29412  cplgr3v  29466  cusgrsizeindslem  29483  sizusglecusglem2  29494  umgr2v2e  29557  cusgrrusgr  29613  iswlk  29642  edginwlk  29667  uspgr2wlkeq  29678  uspgr2wlkeq2  29679  uspgr2wlkeqi  29680  wlkonprop  29690  wlkon2n0  29698  pthdadjvtx  29762  upgr2pthnlp  29764  spthonepeq  29784  pthdlem2lem  29799  crctcshwlkn0lem3  29841  crctcshwlkn0lem5  29843  wlkiswwlks2lem4  29901  wlkiswwlks2lem6  29903  wlklnwwlkln2lem  29911  wwlksnred  29921  wwlksnextbi  29923  wwlksnextwrd  29926  2pthdlem1  29959  2wlkdlem10  29964  umgr2adedgwlkonALT  29976  elwwlks2s3  29980  elwwlks2ons3im  29983  s3wwlks2on  29985  2wspdisj  29991  2wspiundisj  29992  clwwlkgt0  30014  clwlkclwwlklem2a4  30025  clwlkclwwlklem2a  30026  clwlkclwwlk  30030  clwlkclwwlk2  30031  clwlkclwwlkfo  30037  clwwisshclwwslemlem  30041  erclwwlktr  30050  clwwlkf  30075  wwlksubclwwlk  30086  erclwwlkntr  30099  clwwlknon  30118  frcond1  30294  frgr3v  30303  3vfriswmgr  30306  frgrwopreglem4a  30338  frrusgrord0lem  30367  clwwnonrepclwwnon  30373  extwwlkfab  30380  numclwwlk1lem2f1  30385  numclwwlk1lem2fo  30386  clwlknon2num  30396  numclwwlk2lem1  30404  numclwlk2lem2f  30405  numclwlk2lem2f1o  30407  numclwwlk2  30409  frgrreggt1  30421  friendshipgt3  30426  imsmetlem  30718  nmoxr  30794  nmoolb  30799  blometi  30831  phpar2  30851  phpar  30852  ipasslem5  30863  hvadd32  31062  hvaddsub12  31066  hvaddsubass  31069  hvsubass  31072  hvsub32  31073  hvsubdistr1  31077  hvsubdistr2  31078  hvmulcan  31100  hvmulcan2  31101  hvsubcan  31102  his5  31114  his2sub  31120  hhssabloilem  31289  hhssnv  31292  shlej2  31389  pjoi0  31745  hodcl  31775  hoadd32  31811  hosubdi  31836  hosubsub2  31840  hoaddsubass  31843  hosubsub4  31846  nmoplb  31935  unop  31943  hmop  31950  nmfnlb  31952  lnopmul  31995  kbass1  32144  kbass2  32145  leopmul2i  32163  leoptr  32165  cvntr  32320  mdslmd4i  32361  mdexchi  32363  atcv1  32408  sumdmdii  32443  fcoinvbr  32624  fpwrelmapffs  32751  xreceu  32888  isinftm  33170  unitdivcld  33861  esummulc1  34061  hasheuni  34065  unelsiga  34114  inelpisys  34134  carsgsigalem  34296  signswmnd  34550  bnj545  34887  bnj594  34904  bnj1311  35016  fineqvac  35089  usgrgt2cycl  35114  subgrwlk  35116  acycgr1v  35133  cvmsf1o  35256  cvmscld  35257  satefvfmla1  35409  elnanelprv  35413  lediv2aALT  35661  gcd32  35728  fununiq  35749  dfrdg4  35932  brcolinear  36040  colinearex  36041  nn0prpwlem  36304  clsun  36310  fnemeet1  36348  fnemeet2  36349  fnejoin1  36350  fnejoin2  36351  eltail  36356  rdgeqoa  37352  nlpineqsn  37390  curf  37584  lindsadd  37599  poimirlem28  37634  cnambfre  37654  ftc1anclem4  37682  cocanfo  37705  f1ocan1fv  37712  metf1o  37741  ismtybnd  37793  ghomco  37877  isdrngo2  37944  inidl  38016  igenmin  38050  brxrn  38355  brredunds  38607  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  42010  factwoffsmonot  42223  reltsub1  42392  reltsubadd2  42393  resubsub4  42395  reppncan  42399  resubdi  42402  readdcan2  42418  subresre  42436  mapco2g  42701  mzpcompact2lem  42738  eqrabdioph  42764  lerabdioph  42792  eluzrabdioph  42793  ltrabdioph  42795  nerabdioph  42796  dvdsrabdioph  42797  reglogcl  42877  rmxyadd  42909  rmyabs  42946  congadd  42954  congabseq  42962  rmydioph  43002  mendring  43176  mendlmod  43177  iocinico  43200  omge1  43286  relexp0a  43705  relexpaddss  43707  brcoffn  44019  ismnushort  44296  dvconstbi  44329  uzwo4  44992  ssin0  44994  ssinc  45026  ssdec  45027  fvmpt2bd  45112  disjf1o  45133  ssnnf1octb  45136  sub31  45240  fperiodmullem  45253  ssfiunibd  45259  infxr  45316  fmul01  45535  islptre  45574  lptre2pt  45595  limcleqr  45599  limclner  45606  limsuppnflem  45665  limsupvaluz2  45693  supcnvlimsup  45695  xlimmnfvlem2  45788  xlimmnfv  45789  xlimpnfvlem2  45792  xlimpnfv  45793  climxlim2lem  45800  coskpi2  45821  cosknegpi  45824  dvnmptdivc  45893  dvdsn1add  45894  dvnmptconst  45896  dvmptfprod  45900  dvnprodlem1  45901  dvnprodlem2  45902  ovolsplit  45943  stoweidlem60  46015  stowei  46019  dirkeritg  46057  fourierdlem70  46131  fourierdlem71  46132  fourierdlem103  46164  fourierdlem104  46165  fouriersw  46186  rrxtopnfi  46242  saluncl  46272  salexct  46289  sge0ltfirp  46355  sge0iunmpt  46373  meadjiunlem  46420  meaiuninc3v  46439  carageniuncllem1  46476  caratheodorylem1  46481  ovncvrrp  46519  ovnsubaddlem1  46525  hspmbllem2  46582  ovolval5lem3  46609  smfpimbor1lem1  46753  smfsuplem1  46766  smflimsuplem4  46778  sigarls  46812  cnambpcma  47243  elfzelfzlble  47270  submodaddmod  47280  difltmodne  47281  m1mod0mod1  47293  fsumsplitsndif  47297  fundcmpsurinjALT  47336  iccpartiltu  47346  prproropf1olem2  47428  fmtno4prmfac  47496  2pwp1prmfmtno  47514  lighneallem4b  47533  mogoldbblem  47644  gbegt5  47685  sbgoldbm  47708  nnsum3primesle9  47718  nnsum4primesodd  47720  nnsum4primesoddALTV  47721  evengpoap3  47723  nnsum4primesevenALTV  47725  clnbgredg  47763  opstrgric  47832  clnbgrgrimlem  47838  grtrif1o  47846  isubgr3stgrlem1  47868  isubgr3stgrlem4  47871  gpgusgralem  47945  gpg3nbgrvtx0  47966  isupwlk  47979  lidldomnnring  48079  2zrngacmnd  48091  rhmsubcALTVlem2  48125  fprmappr  48189  zlmodzxzscm  48201  gsumlsscl  48224  lincvalsng  48261  lincvalpr  48263  lincdifsn  48269  linc1  48270  lincellss  48271  difmodm1lt  48371  fdivmpt  48389  digexp  48456  2arymaptfo  48503  line  48581  rrxline  48583  itsclc0xyqsolr  48618  iscnrm3r  48744  amgmwlem  49032