Theorem 3adant1 1148

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3ad2ant2  1152  3ad2ant3  1153  3simpc  1168  eupickb  2665  spc3egv  3564  reuhyp  5393  predtrss  6327  onunel  6472  funopg  6574  funprg  6594  funtpg  6595  funcnvtp  6603  unima  6960  fvun1  6976  fnreseql  7047  xpprsng  7140  ftpg  7157  f1ounsn  7276  f13dfv  7278  f1ocoima  7307  f1ofvswap  7310  mpoeq3ia  7494  ordunel  7825  fex2  7935  funexw  7951  poxp  8126  poxp2  8141  poxp3  8148  poseq  8156  suppval1  8164  wfr3g  8318  smores3  8342  oaord  8534  oacan  8535  oaword  8536  omord  8555  omcan  8556  omwordri  8559  odi  8566  omass  8567  oeord  8576  oecan  8577  oewordri  8580  oeordsuc  8582  nnaord  8607  nnaordr  8608  nndi  8611  nnmass  8612  nnaword  8615  nnmord  8620  nnmwordri  8624  naddelim  8675  naddel1  8676  naddel2  8677  naddss1  8678  naddss2  8679  naddasslem2  8684  nadd32  8686  erov  8814  ecopovtrn  8820  ixpf  8920  f1oen4g  8963  f1dom4g  8964  mapxpen  9134  ssfi  9160  sbthfilem  9185  sbthfi  9186  onomeneq  9201  fimax2g  9249  unbnn  9259  funisfsupp  9330  inelfi  9381  elfiun  9393  sup0  9430  suppr  9435  infpr  9468  ttrclss  9692  frr3g  9731  r111  9750  dif1card  10006  ackbij1lem16  10229  cff1  10253  cfflb  10254  cfsmolem  10265  fin23lem34  10341  hsmexlem2  10422  axcc3  10433  domtriomlem  10437  axdc3lem4  10448  axdc4lem  10450  axcclem  10452  konigthlem  10564  gchdomtri  10625  tskpr  10766  tskop  10767  tskuni  10779  tskun  10782  gruop  10801  gruun  10802  grudomon  10813  adderpqlem  10950  mulerpqlem  10951  addassnq  10954  mulassnq  10955  distrnq  10957  ltsonq  10965  ltanq  10967  ltmnq  10968  genpass  11005  distrlem1pr  11021  distrlem4pr  11022  ltsopr  11028  adddir  11208  axlttrn  11293  ltletr  11313  letr  11315  mul32  11387  mul31  11388  add32  11440  subsub23  11473  addsubass  11478  subcan2  11494  subsub2  11497  nppcan2  11500  sub32  11503  nnncan  11504  nnncan2  11506  pnpcan2  11509  subdi  11658  subdir  11659  receu  11870  mulcan1g  11878  mulcan2g  11879  divmul3  11888  divrec  11899  divrec2  11900  div11  11911  divsubdir  11919  subdivcomb2  11922  divdiv1  11937  redivcl  11945  div2neg  11949  ltmul2  12077  lemul1  12078  lemul2  12079  lemul2a  12081  lediv1  12091  gt0div  12092  ge0div  12093  mulsuble0b  12098  ltdivmul  12101  ledivmul  12102  ltdivmul2  12103  ledivmul2  12105  lemuldiv  12106  ltdiv23  12117  lediv23  12118  ledivp1i  12151  ltdivp1i  12152  uzind2  12701  nn0ind  12703  fnn0ind  12707  uz3m2nn  12930  xrltletr  13194  xrletr  13195  xrre2  13208  xrltmin  13220  xrlemin  13222  xleadd2a  13292  xleadd1  13293  xltadd2  13295  xmulasslem3  13324  xmulass  13325  xltmul2  13331  ixxdisj  13399  iooneg  13510  iccneg  13511  icoshft  13512  icoshftf1o  13513  icodisj  13515  snunioo  13517  fzen  13581  ssfzunsnext  13610  fzrev3  13631  2ffzeq  13690  fzoaddel2  13762  elfzodifsumelfzo  13773  ssfzoulel  13802  ssfzo12bi  13803  fzoopth  13804  fzoshftral  13829  adddivflid  13865  flltdivnn0lt  13880  ltdifltdiv  13881  fldiv4p1lem1div2  13882  modcyc  13953  modcyc2  13954  modaddabs  13958  muladdmod  13962  modsubmodmod  13980  modaddmodup  13984  modaddmulmod  13988  moddi  13989  modsubdir  13990  expdiv  14163  digit2  14286  nfile  14409  hashdifpr  14466  hashgt23el  14475  hashreshashfun  14490  hashf1dmcdm  14495  hash3tpexb  14545  fi1uzind  14558  ccatval1  14628  ccatass  14640  swrdval  14697  swrdnd  14710  swrd0  14714  swrdfv2  14717  pfxsuff1eqwrdeq  14754  swrdswrdlem  14759  pfxccatin12lem2a  14782  pfxccatin12lem1  14783  repswccat  14843  cshwidxmod  14860  cshwidxmodr  14861  cshf1  14867  repswcshw  14869  2cshw  14870  2cshwcom  14873  2cshwcshw  14882  cshwcsh2id  14885  ccatco  14892  2swrd2eqwrdeq  15010  wwlktovf  15013  brcnvtrclfv  15060  shftval2  15132  mulre  15192  absdiv  15366  absdiflt  15389  absdifle  15390  abs3dif  15403  cau3  15427  ello12r  15588  elo12r  15599  modfsummods  15864  geoisum1c  15953  rpnnen2lem4  16291  rpnnen2lem7  16294  addmulmodb  16341  dvdsmulc  16359  dvdsmulcr  16361  dvdsmultr1  16372  dvdsmultr2  16374  dvdssub2  16377  oexpneg  16421  divalgb  16480  ndvdsadd  16486  sadass  16547  modgcd  16608  dvdsgcd  16620  dvdsgcdb  16621  gcdass  16623  mulgcd  16624  absmulgcd  16625  rpmulgcd  16633  expgcd  16639  zexpgcd  16641  nn0seqcvgd  16646  algcvga  16655  lcmdvdsb  16689  lcmass  16690  lcmfunsnlem1  16713  lcmfunsnlem2lem1  16714  lcmfunsnlem2lem2  16715  coprmdvds  16729  coprmdvds2  16730  rpmul  16735  cncongr1  16743  cncongr2  16744  qnumdenbi  16821  modprm0  16883  coprimeprodsq  16886  pythagtriplem4  16897  pythagtriplem8  16901  pythagtriplem9  16902  pythagtriplem12  16904  pythagtriplem14  16906  pythagtriplem16  16908  pcpremul  16921  pcgcd  16956  vdwapval  17051  vdwapun  17052  prmgaplem3  17131  prmgaplem4  17132  prmgaplem7  17135  prmgapprmolem  17139  mreiincl  17666  mreincl  17669  mremre  17674  mrcss  17690  catcisolem  18185  pleval2  18409  pospo  18417  latlem  18511  latjcom  18521  latmcom  18537  lubss  18587  lubun  18589  clatglbss  18593  ipole  18608  ipolt  18609  pslem  18646  dirtr  18676  gsumsgrpccat  18923  gsumws2  18925  frmdmnd  18942  symggrplem  18967  isgrpi  19050  grpsubrcan  19111  grpinvsub  19112  grpsubeq0  19116  grpsubadd0sub  19117  grpnpcan  19122  qussub  19286  ghmsub  19318  symgpssefmnd  19490  symggrp  19494  symgextsymg  19518  gsmsymgreqlem2  19525  symgfixfolem1  19532  pmtrprfv3  19548  symggen  19564  lsmass  19763  efgsrel  19828  cntzcmn  19934  dvrcl  20512  unitdvcl  20513  dvrcan1  20517  subrngmre  20691  subrgmre  20726  rhmsubclem2  20815  rrgeq0  20829  abvsubtri  20960  abvtrivd  20965  lmodvsubval2  21068  rmodislmodlem  21080  rmodislmod  21081  lss0cl  21098  lssintcl  21115  lssincl  21116  reslmhm2  21204  lspvadd  21247  lspsntrim  21249  islbs3  21309  unichnlidl  21392  rnglidlmmgm  21409  cncrng  21573  xrsmcmn  21575  cndrng  21581  cnsrng  21586  absabv  21604  xrs1mnd  21620  psgnco  21763  zrhpsgninv  21765  zrhpsgnevpm  21771  zrhpsgnodpm  21772  zrhpsgnelbas  21774  zrhcopsgnelbas  21775  uvcresum  21973  lindfmm  22007  lindsmm  22008  evlsval2  22268  mamudm  22582  mamufacex  22583  matsubgcell  22621  matsc  22637  scmatscmide  22694  scmatrhmcl  22715  1marepvsma1  22770  m1detdiag  22784  mdetralt  22795  m2detleiblem7  22814  gsummatr01lem3  22844  gsummatr01  22846  smadiadetlem0  22848  decpmate  22953  decpmatcl  22954  pm2mpcl  22984  pm2mpghmlem2  22999  chfacfscmul0  23045  chfacfscmulgsum  23047  chfacfpmmul0  23049  chfacfpmmulgsum  23051  unopn  23090  clsss  23241  cldmre  23265  toponmre  23280  opnssneib  23302  restabs  23352  restcls  23368  restntr  23369  hausnei2  23540  cmpsublem  23586  bwth  23597  hausmapdom  23688  ptpjcn  23799  upxp  23811  ptrescn  23827  xkopjcn  23844  fbssfi  24025  snfil  24052  ufprim  24097  rnelfm  24141  flimrest  24171  fclsrest  24212  tmdgsum  24283  blpnfctr  24624  mscl  24649  xmscl  24650  xmsge0  24651  xmseq0  24652  restmetu  24758  ngpds  24792  tngngp3  24844  unitnmn0  24856  xrsxmet  24998  metds0  25039  mpomulcn  25057  cncfmptc  25102  isclmp  25287  cnlmod  25330  ncvsi  25341  cphsqrtcl  25374  cfil3i  25459  cfilres  25486  cmssmscld  25540  cmmbl  25724  voliunlem2  25741  itg2ub  25923  itgrecl  25988  r1pid  26349  eflogeq  26798  cxpadd  26875  cxpcom  26935  logbchbase  26967  relogbreexp  26971  relogbzexp  26972  relogbmulexp  26974  logbleb  26979  logblt  26980  lawcos  27012  pythag  27013  asinsinb  27093  acoscosb  27094  atantanb  27120  amgmlem  27185  lgsneg  27516  lgsne0  27530  lgsmodeq  27537  lgsmulsqcoprm  27538  gausslemma2dlem1a  27560  2sqreulem2  27647  ltsres  27857  noetainflem1  27932  ltlestr  27955  lestr  27957  nocvxmin  27979  madebdaylemold  28122  lrrecpo  28165  ltadds2im  28210  leadds1im  28211  leadds2im  28212  leadds1  28213  leadds2  28214  ltadds1  28216  addscan2  28217  addscan1  28218  subadds  28294  ltsubs1  28300  divscl  28447  oncutlt  28488  zsoring  28633  expscllem  28654  brbtwn2  29286  colinearalg  29291  eleesubd  29293  axcgrrflx  29295  axcgrtr  29296  axsegcon  29308  ax5seglem1  29309  ax5seglem2  29310  ax5seglem4  29313  axbtwnid  29320  axlowdimlem14  29336  axlowdim  29342  axcontlem5  29349  axcontlem7  29351  nb3grprlem2  29765  cplgr3v  29819  cusgrsizeindslem  29835  sizusglecusglem2  29846  umgr2v2e  29909  cusgrrusgr  29965  iswlk  29994  edginwlk  30018  uspgr2wlkeq  30029  uspgr2wlkeq2  30030  uspgr2wlkeqi  30031  wlkonprop  30040  wlkon2n0  30048  subgrwlk  30072  pthdadjvtx  30116  upgr2pthnlp  30121  spthonepeq  30141  pthdlem2lem  30156  crctcshwlkn0lem3  30204  crctcshwlkn0lem5  30206  wlkiswwlks2lem4  30264  wlkiswwlks2lem6  30266  wlklnwwlkln2lem  30274  wwlksnred  30284  wwlksnextbi  30286  wwlksnextwrd  30289  2pthdlem1  30322  2wlkdlem10  30327  umgr2adedgwlkonALT  30339  elwwlks2s3  30343  elwwlks2ons3im  30346  s3wwlks2on  30348  sps3wwlks2on  30349  2wspdisj  30357  2wspiundisj  30358  clwwlkgt0  30380  clwlkclwwlklem2a4  30391  clwlkclwwlklem2a  30392  clwlkclwwlk  30396  clwlkclwwlk2  30397  clwlkclwwlkfo  30403  clwwisshclwwslemlem  30407  erclwwlktr  30416  clwwlkf  30441  wwlksubclwwlk  30452  erclwwlkntr  30465  clwwlknon  30484  frcond1  30664  frgr3v  30673  3vfriswmgr  30676  frgrwopreglem4a  30708  frrusgrord0lem  30737  clwwnonrepclwwnon  30743  extwwlkfab  30750  numclwwlk1lem2f1  30755  numclwwlk1lem2fo  30756  clwlknon2num  30766  numclwwlk2lem1  30774  numclwlk2lem2f  30775  numclwlk2lem2f1o  30777  numclwwlk2  30779  frgrreggt1  30791  friendshipgt3  30796  imsmetlem  31089  nmoxr  31165  nmoolb  31170  blometi  31202  phpar2  31222  phpar  31223  ipasslem5  31234  hvadd32  31433  hvaddsub12  31437  hvaddsubass  31440  hvsubass  31443  hvsub32  31444  hvsubdistr1  31448  hvsubdistr2  31449  hvmulcan  31471  hvmulcan2  31472  hvsubcan  31473  his5  31485  his2sub  31491  hhssabloilem  31660  hhssnv  31663  shlej2  31760  pjoi0  32116  hodcl  32146  hoadd32  32182  hosubdi  32207  hosubsub2  32211  hoaddsubass  32214  hosubsub4  32217  nmoplb  32306  unop  32314  hmop  32321  nmfnlb  32323  lnopmul  32366  kbass1  32515  kbass2  32516  leopmul2i  32534  leoptr  32536  cvntr  32691  mdslmd4i  32732  mdexchi  32734  atcv1  32779  sumdmdii  32814  fcoinvbr  32997  fpwrelmapffs  33125  xreceu  33287  isinftm  33541  inlidl  33769  unitdivcld  34331  esummulc1  34511  hasheuni  34515  unelsiga  34564  inelpisys  34585  carsgsigalem  34746  signswmnd  34985  bnj545  35324  bnj594  35341  bnj1311  35453  fissorduni  35514  r1filimi  35531  fineqvac  35562  fineqvnttrclselem3  35569  fineqvinfep  35571  usgrgt2cycl  35643  acycgr1v  35654  cvmsf1o  35777  cvmscld  35778  satefvfmla1  35930  elnanelprv  35934  lediv2aALT  36182  gcd32  36254  fununiq  36274  dfrdg4  36456  brcolinear  36564  colinearex  36565  ltnmul  36721  ltnadd  36723  nn0prpwlem  36866  clsun  36872  fnemeet1  36910  fnemeet2  36911  fnejoin1  36912  fnejoin2  36913  eltail  36918  rdgeqoa  38049  nlpineqsn  38087  curf  38282  lindsadd  38297  poimirlem28  38332  cnambfre  38352  ftc1anclem4  38380  cocanfo  38403  f1ocan1fv  38410  metf1o  38439  ismtybnd  38491  ghomco  38575  isdrngo2  38642  inidl  38714  igenmin  38748  brxrn  39065  brredunds  39392  cmtvalN  40018  cvrval  40076  pmapmeet  40580  paddval  40605  paddssat  40621  elpcliN  40700  pclssN  40701  pclunN  40705  paddunN  40734  poldmj1N  40735  tendoplcl2  41585  tendoplcl  41588  dihmeet  42150  lcmineqlem1  42829  reltsub1  43180  reltsubadd2  43181  resubsub4  43183  reppncan  43187  resubdi  43190  readdcan2  43207  subresre  43225  mapco2g  43478  mzpcompact2lem  43515  eqrabdioph  43541  lerabdioph  43565  eluzrabdioph  43566  ltrabdioph  43568  nerabdioph  43569  dvdsrabdioph  43570  reglogcl  43650  rmxyadd  43681  rmyabs  43718  congadd  43726  congabseq  43734  rmydioph  43774  mendring  43948  mendlmod  43949  iocinico  43972  omge1  44057  relexp0a  44475  relexpaddss  44477  brcoffn  44789  ismnushort  45044  dvconstbi  45077  uzwo4  45806  ssin0  45808  ssinc  45838  ssdec  45839  fvmpt2bd  45921  disjf1o  45942  ssnnf1octb  45945  sub31  46042  fperiodmullem  46055  ssfiunibd  46061  infxr  46115  fmul01  46329  islptre  46368  lptre2pt  46387  limcleqr  46391  limclner  46398  limsuppnflem  46457  limsupvaluz2  46485  supcnvlimsup  46487  xlimmnfvlem2  46580  xlimmnfv  46581  xlimpnfvlem2  46584  xlimpnfv  46585  climxlim2lem  46592  coskpi2  46613  cosknegpi  46616  dvnmptdivc  46685  dvdsn1add  46686  dvnmptconst  46688  dvmptfprod  46692  dvnprodlem1  46693  dvnprodlem2  46694  ovolsplit  46735  stoweidlem60  46807  stowei  46811  dirkeritg  46849  fourierdlem70  46923  fourierdlem71  46924  fourierdlem103  46956  fourierdlem104  46957  fouriersw  46978  rrxtopnfi  47034  saluncl  47064  salexct  47081  sge0ltfirp  47147  sge0iunmpt  47165  meadjiunlem  47212  meaiuninc3v  47231  carageniuncllem1  47268  caratheodorylem1  47273  ovncvrrp  47311  ovnsubaddlem1  47317  hspmbllem2  47374  ovolval5lem3  47401  smfpimbor1lem1  47545  smfsuplem1  47558  smflimsuplem4  47570  sigarls  47604  cnambpcma  48064  elfzelfzlble  48091  submodaddmod  48117  difltmodne  48118  m1mod0mod1  48130  modmkpkne  48137  mod2addne  48140  modm2nep1  48142  modm1nep2  48144  modm1nem2  48145  fsumsplitsndif  48151  fundcmpsurinjALT  48194  iccpartiltu  48204  prproropf1olem2  48286  fmtno4prmfac  48357  2pwp1prmfmtno  48375  lighneallem4b  48394  nprmdvdsfacm1lem4  48408  mogoldbblem  48518  gbegt5  48559  sbgoldbm  48582  nnsum3primesle9  48592  nnsum4primesodd  48594  nnsum4primesoddALTV  48595  evengpoap3  48597  nnsum4primesevenALTV  48599  clnbgredg  48638  opstrgric  48724  clnbgrgrimlem  48731  grtrif1o  48740  isubgr3stgrlem1  48764  isubgr3stgrlem4  48767  gpgusgralem  48854  gpg3nbgrvtx0  48874  isupwlk  48934  lidldomnnring  49034  2zrngacmnd  49046  rhmsubcALTVlem2  49080  fprmappr  49158  zlmodzxzscm  49170  gsumlsscl  49193  lincvalsng  49229  lincvalpr  49231  lincdifsn  49237  linc1  49238  lincellss  49239  fdivmpt  49353  digexp  49420  2arymaptfo  49467  line  49545  rrxline  49547  itsclc0xyqsolr  49582  iscnrm3r  49759  resipos  49786  amgmwlem  50683