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  2636  spc3egv  3546  sbciegftOLD  3767  reuhyp  5357  predtrss  6280  onunel  6424  funopg  6526  funprg  6546  funtpg  6547  funcnvtp  6555  unima  6909  fvun1  6925  fnreseql  6994  xpprsng  7087  ftpg  7103  f1ounsn  7220  f13dfv  7222  f1ocoima  7251  f1ofvswap  7254  mpoeq3ia  7438  ordunel  7771  fex2  7880  funexw  7898  poxp  8071  poxp2  8086  poxp3  8093  poseq  8101  suppval1  8109  wfr3g  8262  smores3  8286  oaord  8475  oacan  8476  oaword  8477  omord  8496  omcan  8497  omwordri  8500  odi  8507  omass  8508  oeord  8517  oecan  8518  oewordri  8521  oeordsuc  8523  nnaord  8548  nnaordr  8549  nndi  8552  nnmass  8553  nnaword  8556  nnmord  8561  nnmwordri  8565  naddelim  8615  naddel1  8616  naddel2  8617  naddss1  8618  naddss2  8619  naddasslem2  8624  nadd32  8626  erov  8754  ecopovtrn  8760  ixpf  8861  f1oen4g  8904  f1dom4g  8905  mapxpen  9074  ssfi  9100  sbthfilem  9125  sbthfi  9126  onomeneq  9141  fimax2g  9189  unbnn  9199  funisfsupp  9273  inelfi  9324  elfiun  9336  sup0  9373  suppr  9378  infpr  9411  ttrclss  9632  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  10482  gchdomtri  10543  tskpr  10684  tskop  10685  tskuni  10697  tskun  10700  gruop  10719  gruun  10720  grudomon  10731  adderpqlem  10868  mulerpqlem  10869  addassnq  10872  mulassnq  10873  distrnq  10875  ltsonq  10883  ltanq  10885  ltmnq  10886  genpass  10923  distrlem1pr  10939  distrlem4pr  10940  ltsopr  10946  adddir  11126  axlttrn  11209  ltletr  11229  letr  11231  mul32  11303  mul31  11304  add32  11356  subsub23  11389  addsubass  11394  subcan2  11410  subsub2  11413  nppcan2  11416  sub32  11419  nnncan  11420  nnncan2  11422  pnpcan2  11425  subdi  11574  subdir  11575  receu  11786  mulcan1g  11794  mulcan2g  11795  divmul3  11805  divrec  11816  divrec2  11817  div11  11828  divsubdir  11839  subdivcomb2  11842  divdiv1  11857  redivcl  11865  div2neg  11869  ltmul2  11997  lemul1  11998  lemul2  11999  lemul2a  12001  lediv1  12012  gt0div  12013  ge0div  12014  mulsuble0b  12019  ltdivmul  12022  ledivmul  12023  ltdivmul2  12024  ledivmul2  12026  lemuldiv  12027  ltdiv23  12038  lediv23  12039  ledivp1i  12072  ltdivp1i  12073  uzind2  12613  nn0ind  12615  fnn0ind  12619  uz3m2nn  12835  xrltletr  13099  xrletr  13100  xrre2  13113  xrltmin  13125  xrlemin  13127  xleadd2a  13197  xleadd1  13198  xltadd2  13200  xmulasslem3  13229  xmulass  13230  xltmul2  13236  ixxdisj  13304  iooneg  13415  iccneg  13416  icoshft  13417  icoshftf1o  13418  icodisj  13420  snunioo  13422  fzen  13486  ssfzunsnext  13514  fzrev3  13535  2ffzeq  13594  fzoaddel2  13666  elfzodifsumelfzo  13677  ssfzoulel  13706  ssfzo12bi  13707  fzoopth  13708  fzoshftral  13733  adddivflid  13768  flltdivnn0lt  13783  ltdifltdiv  13784  fldiv4p1lem1div2  13785  modcyc  13856  modcyc2  13857  modaddabs  13861  muladdmod  13865  modsubmodmod  13883  modaddmodup  13887  modaddmulmod  13891  moddi  13892  modsubdir  13893  expdiv  14066  digit2  14189  nfile  14312  hashdifpr  14368  hashgt23el  14377  hashreshashfun  14392  hashf1dmcdm  14397  hash3tpexb  14447  fi1uzind  14460  ccatval1  14530  ccatass  14542  swrdval  14597  swrdnd  14608  swrd0  14612  swrdfv2  14615  pfxsuff1eqwrdeq  14652  swrdswrdlem  14657  pfxccatin12lem2a  14680  pfxccatin12lem1  14681  repswccat  14739  cshwidxmod  14756  cshwidxmodr  14757  cshf1  14763  repswcshw  14765  2cshw  14766  2cshwcom  14769  2cshwcshw  14778  cshwcsh2id  14781  ccatco  14788  2swrd2eqwrdeq  14906  wwlktovf  14909  brcnvtrclfv  14956  shftval2  15028  mulre  15074  absdiv  15248  absdiflt  15271  absdifle  15272  abs3dif  15285  cau3  15309  ello12r  15470  elo12r  15481  modfsummods  15747  geoisum1c  15836  rpnnen2lem4  16175  rpnnen2lem7  16178  addmulmodb  16225  dvdsmulc  16243  dvdsmulcr  16245  dvdsmultr1  16256  dvdsmultr2  16258  dvdssub2  16261  oexpneg  16305  divalgb  16364  ndvdsadd  16370  sadass  16431  modgcd  16492  dvdsgcd  16504  dvdsgcdb  16505  gcdass  16507  mulgcd  16508  absmulgcd  16509  rpmulgcd  16517  expgcd  16523  zexpgcd  16525  nn0seqcvgd  16530  algcvga  16539  lcmdvdsb  16573  lcmass  16574  lcmfunsnlem1  16597  lcmfunsnlem2lem1  16598  lcmfunsnlem2lem2  16599  coprmdvds  16613  coprmdvds2  16614  rpmul  16619  cncongr1  16627  cncongr2  16628  qnumdenbi  16705  modprm0  16767  coprimeprodsq  16770  pythagtriplem4  16781  pythagtriplem8  16785  pythagtriplem9  16786  pythagtriplem12  16788  pythagtriplem14  16790  pythagtriplem16  16792  pcpremul  16805  pcgcd  16840  vdwapval  16935  vdwapun  16936  prmgaplem3  17015  prmgaplem4  17016  prmgaplem7  17019  prmgapprmolem  17023  mreiincl  17549  mreincl  17552  mremre  17557  mrcss  17573  catcisolem  18068  pleval2  18292  pospo  18300  latlem  18394  latjcom  18404  latmcom  18420  lubss  18470  lubun  18472  clatglbss  18476  ipole  18491  ipolt  18492  pslem  18529  dirtr  18559  gsumsgrpccat  18799  gsumws2  18801  frmdmnd  18818  symggrplem  18843  isgrpi  18926  grpsubrcan  18988  grpinvsub  18989  grpsubeq0  18993  grpsubadd0sub  18994  grpnpcan  18999  qussub  19157  ghmsub  19190  symgpssefmnd  19362  symggrp  19366  symgextsymg  19390  gsmsymgreqlem2  19397  symgfixfolem1  19404  pmtrprfv3  19420  symggen  19436  lsmass  19635  efgsrel  19700  cntzcmn  19806  dvrcl  20375  unitdvcl  20376  dvrcan1  20380  subrngmre  20530  subrgmre  20565  rhmsubclem2  20654  rrgeq0  20668  abvsubtri  20795  abvtrivd  20800  lmodvsubval2  20903  rmodislmodlem  20915  rmodislmod  20916  lss0cl  20933  lssintcl  20950  lssincl  20951  reslmhm2  21040  lspvadd  21083  lspsntrim  21085  islbs3  21145  rnglidlmmgm  21235  cncrng  21378  cncrngOLD  21379  xrsmcmn  21381  cndrng  21388  cndrngOLD  21389  cnsrng  21395  absabv  21414  xrs1mnd  21430  psgnco  21573  zrhpsgninv  21575  zrhpsgnevpm  21581  zrhpsgnodpm  21582  zrhpsgnelbas  21584  zrhcopsgnelbas  21585  uvcresum  21783  lindfmm  21817  lindsmm  21818  evlsval2  22075  mamudm  22370  mamufacex  22371  matsubgcell  22409  matsc  22425  scmatscmide  22482  scmatrhmcl  22503  1marepvsma1  22558  m1detdiag  22572  mdetralt  22583  m2detleiblem7  22602  gsummatr01lem3  22632  gsummatr01  22634  smadiadetlem0  22636  decpmate  22741  decpmatcl  22742  pm2mpcl  22772  pm2mpghmlem2  22787  chfacfscmul0  22833  chfacfscmulgsum  22835  chfacfpmmul0  22837  chfacfpmmulgsum  22839  unopn  22878  clsss  23029  cldmre  23053  toponmre  23068  opnssneib  23090  restabs  23140  restcls  23156  restntr  23157  hausnei2  23328  cmpsublem  23374  bwth  23385  hausmapdom  23475  ptpjcn  23586  upxp  23598  ptrescn  23614  xkopjcn  23631  fbssfi  23812  snfil  23839  ufprim  23884  rnelfm  23928  flimrest  23958  fclsrest  23999  tmdgsum  24070  blpnfctr  24411  mscl  24436  xmscl  24437  xmsge0  24438  xmseq0  24439  restmetu  24545  ngpds  24579  tngngp3  24631  unitnmn0  24643  xrsxmet  24785  metds0  24826  mpomulcn  24844  cncfmptc  24889  isclmp  25074  cnlmod  25117  ncvsi  25128  cphsqrtcl  25161  cfil3i  25246  cfilres  25273  cmssmscld  25327  cmmbl  25511  voliunlem2  25528  itg2ub  25710  itgrecl  25775  r1pid  26136  eflogeq  26579  cxpadd  26656  cxpcom  26716  logbchbase  26748  relogbreexp  26752  relogbzexp  26753  relogbmulexp  26755  logbleb  26760  logblt  26761  lawcos  26793  pythag  26794  asinsinb  26874  acoscosb  26875  atantanb  26901  amgmlem  26967  lgsneg  27298  lgsne0  27312  lgsmodeq  27319  lgsmulsqcoprm  27320  gausslemma2dlem1a  27342  2sqreulem2  27429  ltsres  27640  noetainflem1  27715  ltlestr  27738  lestr  27740  nocvxmin  27761  madebdaylemold  27904  lrrecpo  27947  ltadds2im  27992  leadds1im  27993  leadds2im  27994  leadds1  27995  leadds2  27996  ltadds1  27998  addscan2  27999  addscan1  28000  subadds  28076  ltsubs1  28082  divscl  28229  oncutlt  28270  zsoring  28415  expscllem  28436  brbtwn2  28988  colinearalg  28993  eleesubd  28995  axcgrrflx  28997  axcgrtr  28998  axsegcon  29010  ax5seglem1  29011  ax5seglem2  29012  ax5seglem4  29015  axbtwnid  29022  axlowdimlem14  29038  axlowdim  29044  axcontlem5  29051  axcontlem7  29053  nb3grprlem2  29464  cplgr3v  29518  cusgrsizeindslem  29535  sizusglecusglem2  29546  umgr2v2e  29609  cusgrrusgr  29665  iswlk  29694  edginwlk  29718  uspgr2wlkeq  29729  uspgr2wlkeq2  29730  uspgr2wlkeqi  29731  wlkonprop  29740  wlkon2n0  29748  pthdadjvtx  29811  upgr2pthnlp  29815  spthonepeq  29835  pthdlem2lem  29850  crctcshwlkn0lem3  29895  crctcshwlkn0lem5  29897  wlkiswwlks2lem4  29955  wlkiswwlks2lem6  29957  wlklnwwlkln2lem  29965  wwlksnred  29975  wwlksnextbi  29977  wwlksnextwrd  29980  2pthdlem1  30013  2wlkdlem10  30018  umgr2adedgwlkonALT  30030  elwwlks2s3  30034  elwwlks2ons3im  30037  s3wwlks2on  30039  sps3wwlks2on  30040  2wspdisj  30048  2wspiundisj  30049  clwwlkgt0  30071  clwlkclwwlklem2a4  30082  clwlkclwwlklem2a  30083  clwlkclwwlk  30087  clwlkclwwlk2  30088  clwlkclwwlkfo  30094  clwwisshclwwslemlem  30098  erclwwlktr  30107  clwwlkf  30132  wwlksubclwwlk  30143  erclwwlkntr  30156  clwwlknon  30175  frcond1  30351  frgr3v  30360  3vfriswmgr  30363  frgrwopreglem4a  30395  frrusgrord0lem  30424  clwwnonrepclwwnon  30430  extwwlkfab  30437  numclwwlk1lem2f1  30442  numclwwlk1lem2fo  30443  clwlknon2num  30453  numclwwlk2lem1  30461  numclwlk2lem2f  30462  numclwlk2lem2f1o  30464  numclwwlk2  30466  frgrreggt1  30478  friendshipgt3  30483  imsmetlem  30776  nmoxr  30852  nmoolb  30857  blometi  30889  phpar2  30909  phpar  30910  ipasslem5  30921  hvadd32  31120  hvaddsub12  31124  hvaddsubass  31127  hvsubass  31130  hvsub32  31131  hvsubdistr1  31135  hvsubdistr2  31136  hvmulcan  31158  hvmulcan2  31159  hvsubcan  31160  his5  31172  his2sub  31178  hhssabloilem  31347  hhssnv  31350  shlej2  31447  pjoi0  31803  hodcl  31833  hoadd32  31869  hosubdi  31894  hosubsub2  31898  hoaddsubass  31901  hosubsub4  31904  nmoplb  31993  unop  32001  hmop  32008  nmfnlb  32010  lnopmul  32053  kbass1  32202  kbass2  32203  leopmul2i  32221  leoptr  32223  cvntr  32378  mdslmd4i  32419  mdexchi  32421  atcv1  32466  sumdmdii  32501  fcoinvbr  32690  fpwrelmapffs  32822  xreceu  32996  isinftm  33257  unitdivcld  34061  esummulc1  34241  hasheuni  34245  unelsiga  34294  inelpisys  34314  carsgsigalem  34475  signswmnd  34717  bnj545  35053  bnj594  35070  bnj1311  35182  fissorduni  35249  r1filimi  35262  fineqvac  35276  fineqvnttrclselem3  35283  fineqvinfep  35285  usgrgt2cycl  35328  subgrwlk  35330  acycgr1v  35347  cvmsf1o  35470  cvmscld  35471  satefvfmla1  35623  elnanelprv  35627  lediv2aALT  35875  gcd32  35947  fununiq  35967  dfrdg4  36149  brcolinear  36257  colinearex  36258  nn0prpwlem  36520  clsun  36526  fnemeet1  36564  fnemeet2  36565  fnejoin1  36566  fnejoin2  36567  eltail  36572  rdgeqoa  37700  nlpineqsn  37738  curf  37933  lindsadd  37948  poimirlem28  37983  cnambfre  38003  ftc1anclem4  38031  cocanfo  38054  f1ocan1fv  38061  metf1o  38090  ismtybnd  38142  ghomco  38226  isdrngo2  38293  inidl  38365  igenmin  38399  brxrn  38718  brredunds  39045  cmtvalN  39671  cvrval  39729  pmapmeet  40233  paddval  40258  paddssat  40274  elpcliN  40353  pclssN  40354  pclunN  40358  paddunN  40387  poldmj1N  40388  tendoplcl2  41238  tendoplcl  41241  dihmeet  41803  lcmineqlem1  42482  reltsub1  42832  reltsubadd2  42833  resubsub4  42835  reppncan  42839  resubdi  42842  readdcan2  42859  subresre  42877  mapco2g  43160  mzpcompact2lem  43197  eqrabdioph  43223  lerabdioph  43251  eluzrabdioph  43252  ltrabdioph  43254  nerabdioph  43255  dvdsrabdioph  43256  reglogcl  43336  rmxyadd  43367  rmyabs  43404  congadd  43412  congabseq  43420  rmydioph  43460  mendring  43634  mendlmod  43635  iocinico  43658  omge1  43743  relexp0a  44161  relexpaddss  44163  brcoffn  44475  ismnushort  44746  dvconstbi  44779  uzwo4  45502  ssin0  45504  ssinc  45535  ssdec  45536  fvmpt2bd  45618  disjf1o  45639  ssnnf1octb  45642  sub31  45741  fperiodmullem  45754  ssfiunibd  45760  infxr  45814  fmul01  46028  islptre  46067  lptre2pt  46086  limcleqr  46090  limclner  46097  limsuppnflem  46156  limsupvaluz2  46184  supcnvlimsup  46186  xlimmnfvlem2  46279  xlimmnfv  46280  xlimpnfvlem2  46283  xlimpnfv  46284  climxlim2lem  46291  coskpi2  46312  cosknegpi  46315  dvnmptdivc  46384  dvdsn1add  46385  dvnmptconst  46387  dvmptfprod  46391  dvnprodlem1  46392  dvnprodlem2  46393  ovolsplit  46434  stoweidlem60  46506  stowei  46510  dirkeritg  46548  fourierdlem70  46622  fourierdlem71  46623  fourierdlem103  46655  fourierdlem104  46656  fouriersw  46677  rrxtopnfi  46733  saluncl  46763  salexct  46780  sge0ltfirp  46846  sge0iunmpt  46864  meadjiunlem  46911  meaiuninc3v  46930  carageniuncllem1  46967  caratheodorylem1  46972  ovncvrrp  47010  ovnsubaddlem1  47016  hspmbllem2  47073  ovolval5lem3  47100  smfpimbor1lem1  47244  smfsuplem1  47257  smflimsuplem4  47269  sigarls  47303  cnambpcma  47754  elfzelfzlble  47781  submodaddmod  47807  difltmodne  47808  m1mod0mod1  47820  modmkpkne  47827  mod2addne  47830  modm2nep1  47832  modm1nep2  47834  modm1nem2  47835  fsumsplitsndif  47841  fundcmpsurinjALT  47884  iccpartiltu  47894  prproropf1olem2  47976  fmtno4prmfac  48047  2pwp1prmfmtno  48065  lighneallem4b  48084  nprmdvdsfacm1lem4  48098  mogoldbblem  48208  gbegt5  48249  sbgoldbm  48272  nnsum3primesle9  48282  nnsum4primesodd  48284  nnsum4primesoddALTV  48285  evengpoap3  48287  nnsum4primesevenALTV  48289  clnbgredg  48328  opstrgric  48414  clnbgrgrimlem  48421  grtrif1o  48430  isubgr3stgrlem1  48454  isubgr3stgrlem4  48457  gpgusgralem  48544  gpg3nbgrvtx0  48564  isupwlk  48624  lidldomnnring  48724  2zrngacmnd  48736  rhmsubcALTVlem2  48770  fprmappr  48833  zlmodzxzscm  48845  gsumlsscl  48868  lincvalsng  48904  lincvalpr  48906  lincdifsn  48912  linc1  48913  lincellss  48914  fdivmpt  49028  digexp  49095  2arymaptfo  49142  line  49220  rrxline  49222  itsclc0xyqsolr  49257  iscnrm3r  49435  resipos  49462  amgmwlem  50289