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  2663  spc3egv  3561  rspc2ev  3592  reuhyp  5389  predtrss  6351  onunel  6496  fununiq  6583  funopg  6602  funprg  6624  funtpg  6625  funcnvtp  6633  unima  6991  fvun1  7007  fnreseql  7078  xpprsng  7174  ftpg  7192  f1ounsn  7311  f13dfv  7313  f1ocoima  7342  f1ofvswap  7345  mpoeq3ia  7529  ordunel  7872  fex2  7982  funexw  7998  poxp  8177  poxp2  8197  poxp3  8204  poseq  8212  suppval1  8221  wfr3g  8375  smores3  8399  oaord  8593  oacan  8594  oaword  8595  omord  8614  omcan  8615  omwordri  8618  odi  8625  omass  8626  oeord  8635  oecan  8636  oewordri  8639  oeordsuc  8641  nnaord  8666  nnaordr  8667  nndi  8670  nnmass  8671  nnaword  8674  nnmord  8679  nnmwordri  8683  naddelim  8734  naddel1  8735  naddel2  8736  naddss1  8737  naddss2  8738  naddasslem2  8743  nadd32  8745  erov  8873  ecopovtrn  8879  curf  8928  ixpf  8986  f1oen4g  9029  f1dom4g  9030  mapxpen  9200  ssfi  9226  sbthfilem  9251  sbthfi  9252  onomeneq  9267  fimax2g  9315  fissorduni  9320  unbnn  9326  funisfsupp  9397  inelfi  9447  elfiun  9459  sup0  9496  suppr  9501  infpr  9534  ttrclss  9758  frr3g  9797  r111  9819  r1filimi  9940  dif1card  10128  ackbij1lem16  10351  cff1  10375  cfflb  10376  cfsmolem  10387  fin23lem34  10463  hsmexlem2  10544  axcc3  10555  domtriomlem  10559  axdc3lem4  10570  axdc4lem  10572  axcclem  10574  konigthlem  10692  gchdomtri  10753  tskpr  10894  tskop  10895  tskuni  10907  tskun  10910  gruop  10929  gruun  10930  grudomon  10941  adderpqlem  11078  mulerpqlem  11079  addassnq  11082  mulassnq  11083  distrnq  11085  ltsonq  11093  ltanq  11095  ltmnq  11096  genpass  11133  distrlem1pr  11149  distrlem4pr  11150  ltsopr  11156  adddir  11336  axlttrn  11421  ltletr  11441  letr  11443  mul32  11515  mul31  11516  add32  11568  subsub23  11601  addsubass  11606  subcan2  11622  subsub2  11625  nppcan2  11628  sub32  11631  nnncan  11632  nnncan2  11634  pnpcan2  11637  subdi  11788  subdir  11789  receu  12001  mulcan1g  12009  mulcan2g  12010  divmul3  12019  divrec  12030  divrec2  12031  div11  12042  divsubdir  12050  subdivcomb2  12053  divdiv1  12068  redivcl  12076  div2neg  12080  ltmul2  12208  lemul1  12209  lemul2  12210  lemul2a  12212  lediv1  12222  gt0div  12223  ge0div  12224  mulsuble0b  12229  ltdivmul  12232  ledivmul  12233  ltdivmul2  12234  ledivmul2  12236  lemuldiv  12237  ltdiv23  12248  lediv23  12249  ledivp1i  12282  ltdivp1i  12283  uzind2  12832  nn0ind  12834  fnn0ind  12838  uz3m2nn  13061  xrltletr  13326  xrletr  13327  xrre2  13340  xrltmin  13352  xrlemin  13354  xleadd2a  13424  xleadd1  13425  xltadd2  13427  xmulasslem3  13456  xmulass  13457  xltmul2  13463  ixxdisj  13531  iooneg  13642  iccneg  13643  icoshft  13644  icoshftf1o  13645  icodisj  13647  snunioo  13649  fzen  13714  ssfzunsnext  13743  fzrev3  13764  2ffzeq  13823  fzoaddel2  13895  elfzodifsumelfzo  13906  ssfzoulel  13935  ssfzo12bi  13936  fzoopth  13937  fzoshftral  13962  adddivflid  13998  flltdivnn0lt  14013  ltdifltdiv  14014  fldiv4p1lem1div2  14015  modcyc  14086  modcyc2  14087  modaddabs  14091  muladdmod  14095  modsubmodmod  14113  modaddmodup  14117  modaddmulmod  14121  moddi  14122  modsubdir  14123  expdiv  14296  digit2  14421  nfile  14544  hashdifpr  14601  hashgt23el  14610  hashreshashfun  14625  hashf1dmcdm  14630  hash3tpexb  14680  fi1uzind  14693  ccatval1  14763  ccatass  14775  swrdval  14833  swrdnd  14846  swrd0  14850  swrdfv2  14853  pfxsuff1eqwrdeq  14890  swrdswrdlem  14895  pfxccatin12lem2a  14918  pfxccatin12lem1  14919  repswccat  14979  cshwidxmod  14996  cshwidxmodr  14997  cshf1  15003  repswcshw  15005  2cshw  15006  2cshwcom  15009  2cshwcshw  15018  cshwcsh2id  15021  ccatco  15028  2swrd2eqwrdeq  15149  wwlktovf  15152  brcnvtrclfv  15199  shftval2  15271  mulre  15331  absdiv  15505  absdiflt  15528  absdifle  15529  abs3dif  15542  cau3  15567  ello12r  15728  elo12r  15739  modfsummods  16004  geoisum1c  16093  rpnnen2lem4  16429  rpnnen2lem7  16432  addmulmodb  16479  dvdsmulc  16497  dvdsmulcr  16499  dvdsmultr1  16510  dvdsmultr2  16512  dvdssub2  16515  oexpneg  16559  divalgb  16618  ndvdsadd  16624  sadass  16685  modgcd  16749  dvdsgcd  16761  dvdsgcdb  16762  gcdass  16764  mulgcd  16765  absmulgcd  16766  rpmulgcd  16775  expgcd  16781  zexpgcd  16783  nn0seqcvgd  16789  algcvga  16798  lcmdvdsb  16832  lcmass  16833  lcmfunsnlem1  16856  lcmfunsnlem2lem1  16857  lcmfunsnlem2lem2  16858  coprmdvds  16872  coprmdvds2  16873  rpmul  16878  cncongr1  16886  cncongr2  16887  qnumdenbi  16964  modprm0  17027  coprimeprodsq  17030  pythagtriplem4  17041  pythagtriplem8  17045  pythagtriplem9  17046  pythagtriplem12  17048  pythagtriplem14  17050  pythagtriplem16  17052  pcpremul  17065  pcgcd  17100  vdwapval  17195  vdwapun  17196  prmgaplem3  17275  prmgaplem4  17276  prmgaplem7  17279  prmgapprmolem  17283  mreiincl  17816  mreincl  17819  mremre  17824  mrcss  17840  catcisolem  18335  pleval2  18559  pospo  18567  latlem  18661  latjcom  18671  latmcom  18687  lubss  18737  lubun  18739  clatglbss  18743  ipole  18758  ipolt  18759  pslem  18796  dirtr  18826  gsumsgrpccat  19086  gsumws2  19088  frmdmnd  19105  symggrplem  19130  isgrpi  19220  grpsubrcan  19281  grpinvsub  19282  grpsubeq0  19286  grpsubadd0sub  19287  grpnpcan  19292  qussub  19456  ghmsub  19488  symgpssefmnd  19661  symggrp  19665  symgextsymg  19689  gsmsymgreqlem2  19696  symgfixfolem1  19703  pmtrprfv3  19719  symggen  19735  lsmass  19934  efgsrel  19999  cntzcmn  20105  dvrcl  20685  unitdvcl  20686  dvrcan1  20690  subrngmre  20865  subrgmre  20900  rhmsubclem2  20989  rrgeq0  21003  abvsubtri  21135  abvtrivd  21140  lmodvsubval2  21243  rmodislmodlem  21255  rmodislmod  21256  lss0cl  21273  lssintcl  21290  lssincl  21291  reslmhm2  21379  lspvadd  21422  lspsntrim  21424  islbs3  21484  unichnlidl  21567  rnglidlmmgm  21584  cncrng  21751  xrsmcmn  21753  cndrng  21759  cnsrng  21764  absabv  21784  xrs1mnd  21800  psgnco  21944  zrhpsgninv  21946  zrhpsgnevpm  21952  zrhpsgnodpm  21953  zrhpsgnelbas  21955  zrhcopsgnelbas  21956  uvcresum  22154  lindfmm  22188  lindsmm  22189  evlsval2  22451  mamudm  22765  mamufacex  22766  matsubgcell  22804  matsc  22820  scmatscmide  22877  scmatrhmcl  22898  1marepvsma1  22953  m1detdiag  22967  mdetralt  22978  m2detleiblem7  22997  gsummatr01lem3  23027  gsummatr01  23029  smadiadetlem0  23031  decpmate  23139  decpmatcl  23140  pm2mpcl  23170  pm2mpghmlem2  23185  chfacfscmul0  23231  chfacfscmulgsum  23233  chfacfpmmul0  23235  chfacfpmmulgsum  23237  unopn  23276  clsss  23427  cldmre  23451  toponmre  23466  opnssneib  23488  restabs  23538  restcls  23554  restntr  23555  hausnei2  23726  cmpsublem  23772  bwth  23783  hausmapdom  23874  ptpjcn  23985  upxp  23997  ptrescn  24013  xkopjcn  24030  fbssfi  24211  snfil  24238  ufprim  24283  rnelfm  24327  flimrest  24357  fclsrest  24398  tmdgsum  24469  blpnfctr  24810  mscl  24835  xmscl  24836  xmsge0  24837  xmseq0  24838  restmetu  24944  ngpds  24978  tngngp3  25030  unitnmn0  25042  xrsxmet  25184  metds0  25225  mpomulcn  25243  cncfmptc  25288  isclmp  25473  cnlmod  25516  ncvsi  25527  cphsqrtcl  25560  cfil3i  25645  cfilres  25672  cmssmscld  25726  cmmbl  25910  voliunlem2  25927  itg2ub  26109  itgrecl  26173  r1pid  26534  eflogeq  26987  cxpadd  27064  cxpcom  27124  logbchbase  27156  relogbreexp  27160  relogbzexp  27161  relogbmulexp  27163  logbleb  27168  logblt  27169  lawcos  27201  pythag  27202  asinsinb  27282  acoscosb  27283  atantanb  27309  amgmlem  27374  lgsneg  27705  lgsne0  27719  lgsmodeq  27726  lgsmulsqcoprm  27727  gausslemma2dlem1a  27749  2sqreulem2  27836  ltsres  28076  noetainflem1  28151  ltlestr  28174  lestr  28176  nocvxmin  28198  madebdaylemold  28341  lrrecpo  28384  ltadds2im  28429  leadds1im  28430  leadds2im  28431  leadds1  28432  leadds2  28433  ltadds1  28435  addscan2  28436  addscan1  28437  subadds  28513  ltsubs1  28519  divscl  28666  oncutlt  28707  zsoring  28852  expscllem  28873  brbtwn2  29540  colinearalg  29545  eleesubd  29547  axcgrrflx  29549  axcgrtr  29550  axsegcon  29562  ax5seglem1  29563  ax5seglem2  29564  ax5seglem4  29567  axbtwnid  29574  axlowdimlem14  29590  axlowdim  29596  axcontlem5  29603  axcontlem7  29605  nb3grprlem2  30019  cplgr3v  30073  cusgrsizeindslem  30089  sizusglecusglem2  30100  umgr2v2e  30163  cusgrrusgr  30219  iswlk  30248  edginwlk  30272  uspgr2wlkeq  30283  uspgr2wlkeq2  30284  uspgr2wlkeqi  30285  wlkonprop  30294  wlkon2n0  30302  subgrwlk  30326  pthdadjvtx  30370  upgr2pthnlp  30375  spthonepeq  30395  pthdlem2lem  30410  crctcshwlkn0lem3  30458  crctcshwlkn0lem5  30460  wlkiswwlks2lem4  30518  wlkiswwlks2lem6  30520  wlklnwwlkln2lem  30528  wwlksnred  30538  wwlksnextbi  30540  wwlksnextwrd  30543  2pthdlem1  30576  2wlkdlem10  30581  umgr2adedgwlkonALT  30593  elwwlks2s3  30597  elwwlks2ons3im  30600  s3wwlks2on  30602  sps3wwlks2on  30603  2wspdisj  30611  2wspiundisj  30612  clwwlkgt0  30634  clwlkclwwlklem2a4  30645  clwlkclwwlklem2a  30646  clwlkclwwlk  30650  clwlkclwwlk2  30651  clwlkclwwlkfo  30657  clwwisshclwwslemlem  30661  erclwwlktr  30670  clwwlkf  30695  wwlksubclwwlk  30706  erclwwlkntr  30719  clwwlknon  30738  frcond1  30924  frgr3v  30933  3vfriswmgr  30936  frgrwopreglem4a  30968  frrusgrord0lem  30997  clwwnonrepclwwnon  31003  extwwlkfab  31010  numclwwlk1lem2f1  31015  numclwwlk1lem2fo  31016  clwlknon2num  31026  numclwwlk2lem1  31034  numclwlk2lem2f  31035  numclwlk2lem2f1o  31037  numclwwlk2  31039  frgrreggt1  31051  friendshipgt3  31056  imsmetlem  31349  nmoxr  31425  nmoolb  31430  blometi  31462  phpar2  31482  phpar  31483  ipasslem5  31494  hvadd32  31693  hvaddsub12  31697  hvaddsubass  31700  hvsubass  31703  hvsub32  31704  hvsubdistr1  31708  hvsubdistr2  31709  hvmulcan  31731  hvmulcan2  31732  hvsubcan  31733  his5  31745  his2sub  31751  hhssabloilem  31920  hhssnv  31923  shlej2  32020  pjoi0  32376  hodcl  32406  hoadd32  32442  hosubdi  32467  hosubsub2  32471  hoaddsubass  32474  hosubsub4  32477  nmoplb  32566  unop  32574  hmop  32581  nmfnlb  32583  lnopmul  32626  kbass1  32775  kbass2  32776  leopmul2i  32794  leoptr  32796  cvntr  32951  mdslmd4i  32992  mdexchi  32994  atcv1  33039  sumdmdii  33074  fcoinvbr  33297  fpwrelmapffs  33422  xreceu  33584  isinftm  33841  inlidl  34075  unitdivcld  34644  esummulc1  34824  hasheuni  34828  unelsiga  34877  inelpisys  34898  carsgsigalem  35058  signswmnd  35297  bnj545  35636  bnj594  35653  bnj1311  35765  weexenwe  35889  fineqvac  35925  fineqvnttrclselem3  35932  fineqvinfep  35934  onprcf1acwevdlem1  36086  usgrgt2cycl  36107  acycgr1v  36112  cvmsf1o  36245  cvmscld  36246  satefvfmla1  36398  elnanelprv  36402  lediv2aALT  36650  gcd32  36729  dfrdg4  36930  brcolinear  37039  colinearex  37040  ltnmul  37180  ltnadd  37182  nn0prpwlem  37325  clsun  37331  fnemeet1  37369  fnemeet2  37370  fnejoin1  37371  fnejoin2  37372  eltail  37377  rdgeqoa  38561  nlpineqsn  38599  lindsadd  38804  poimirlem28  38834  cnambfre  38854  ftc1anclem4  38882  cocanfo  38921  f1ocan1fv  38928  metf1o  38955  ismtybnd  39007  ghomco  39091  isdrngo2  39158  inidl  39230  igenmin  39264  brxrn  39581  brredunds  39908  cmtvalN  40534  cvrval  40592  pmapmeet  41096  paddval  41121  paddssat  41137  elpcliN  41216  pclssN  41217  pclunN  41221  paddunN  41250  poldmj1N  41251  tendoplcl2  42101  tendoplcl  42104  dihmeet  42666  lcmineqlem1  43345  reltsub1  43703  reltsubadd2  43704  resubsub4  43706  reppncan  43710  resubdi  43713  readdcan2  43730  subresre  43748  mapco2g  43991  mzpcompact2lem  44028  eqrabdioph  44054  lerabdioph  44078  eluzrabdioph  44079  ltrabdioph  44081  nerabdioph  44082  dvdsrabdioph  44083  reglogcl  44163  rmxyadd  44194  rmyabs  44231  congadd  44239  congabseq  44247  rmydioph  44287  mendring  44451  mendlmod  44452  iocinico  44475  omge1  44560  relexp0a  44977  relexpaddss  44979  brcoffn  45291  ismnushort  45546  dvconstbi  45579  uzwo4  46344  ssin0  46346  ssinc  46375  ssdec  46376  fvmpt2bd  46458  disjf1o  46479  ssnnf1octb  46482  sub31  46579  fperiodmullem  46592  ssfiunibd  46598  infxr  46651  fmul01  46865  islptre  46904  lptre2pt  46923  limcleqr  46927  limclner  46934  limsuppnflem  46993  limsupvaluz2  47021  supcnvlimsup  47023  xlimmnfvlem2  47116  xlimmnfv  47117  xlimpnfvlem2  47120  xlimpnfv  47121  climxlim2lem  47128  coskpi2  47149  cosknegpi  47152  dvnmptdivc  47221  dvdsn1add  47222  dvnmptconst  47224  dvmptfprod  47228  dvnprodlem1  47229  dvnprodlem2  47230  ovolsplit  47271  stoweidlem60  47343  stowei  47347  dirkeritg  47385  fourierdlem70  47459  fourierdlem71  47460  fourierdlem103  47492  fourierdlem104  47493  fouriersw  47514  rrxtopnfi  47570  saluncl  47600  salexct  47617  sge0ltfirp  47683  sge0iunmpt  47701  meadjiunlem  47748  meaiuninc3v  47767  carageniuncllem1  47804  caratheodorylem1  47809  ovncvrrp  47847  ovnsubaddlem1  47853  hspmbllem2  47910  ovolval5lem3  47937  smfpimbor1lem1  48081  smfsuplem1  48094  smflimsuplem4  48106  sigarls  48140  cnambpcma  48637  elfzelfzlble  48664  submodaddmod  48690  difltmodne  48691  m1mod0mod1  48703  modmkpkne  48710  mod2addne  48713  modm2nep1  48715  modm1nep2  48717  modm1nem2  48718  fsumsplitsndif  48724  fundcmpsurinjALT  48767  iccpartiltu  48777  prproropf1olem2  48859  fmtno4prmfac  48930  2pwp1prmfmtno  48948  lighneallem4b  48967  nprmdvdsfacm1lem4  48981  mogoldbblem  49091  gbegt5  49132  sbgoldbm  49155  nnsum3primesle9  49165  nnsum4primesodd  49167  nnsum4primesoddALTV  49168  evengpoap3  49170  nnsum4primesevenALTV  49172  clnbgredg  49211  opstrgric  49297  clnbgrgrimlem  49304  grtrif1o  49313  isubgr3stgrlem1  49337  isubgr3stgrlem4  49340  gpgusgralem  49427  gpg3nbgrvtx0  49447  isupwlk  49507  lidldomnnring  49606  2zrngacmnd  49618  rhmsubcALTVlem2  49652  fprmappr  49788  zlmodzxzscm  49800  gsumlsscl  49823  lincvalsng  49859  lincvalpr  49861  lincdifsn  49867  linc1  49868  lincellss  49869  fdivmpt  49983  digexp  50050  2arymaptfo  50097  line  50176  rrxline  50178  itsclc0xyqsolr  50212  iscnrm3r  50393  resipos  50420  amgmwlem  51415