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  2660  spc3egv  3557  reuhyp  5385  predtrss  6320  onunel  6465  funopg  6567  funprg  6587  funtpg  6588  funcnvtp  6596  unima  6953  fvun1  6969  fnreseql  7040  xpprsng  7135  ftpg  7153  f1ounsn  7273  f13dfv  7275  f1ocoima  7304  f1ofvswap  7307  mpoeq3ia  7491  ordunel  7823  fex2  7933  funexw  7949  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  curf  8869  ixpf  8927  f1oen4g  8970  f1dom4g  8971  mapxpen  9141  ssfi  9167  sbthfilem  9192  sbthfi  9193  onomeneq  9208  fimax2g  9256  unbnn  9266  funisfsupp  9337  inelfi  9388  elfiun  9400  sup0  9437  suppr  9442  infpr  9475  ttrclss  9699  frr3g  9738  r111  9757  dif1card  10013  ackbij1lem16  10236  cff1  10260  cfflb  10261  cfsmolem  10272  fin23lem34  10348  hsmexlem2  10429  axcc3  10440  domtriomlem  10444  axdc3lem4  10455  axdc4lem  10457  axcclem  10459  konigthlem  10577  gchdomtri  10638  tskpr  10779  tskop  10780  tskuni  10792  tskun  10795  gruop  10814  gruun  10815  grudomon  10826  adderpqlem  10963  mulerpqlem  10964  addassnq  10967  mulassnq  10968  distrnq  10970  ltsonq  10978  ltanq  10980  ltmnq  10981  genpass  11018  distrlem1pr  11034  distrlem4pr  11035  ltsopr  11041  adddir  11221  axlttrn  11306  ltletr  11326  letr  11328  mul32  11400  mul31  11401  add32  11453  subsub23  11486  addsubass  11491  subcan2  11507  subsub2  11510  nppcan2  11513  sub32  11516  nnncan  11517  nnncan2  11519  pnpcan2  11522  subdi  11671  subdir  11672  receu  11883  mulcan1g  11891  mulcan2g  11892  divmul3  11901  divrec  11912  divrec2  11913  div11  11924  divsubdir  11932  subdivcomb2  11935  divdiv1  11950  redivcl  11958  div2neg  11962  ltmul2  12090  lemul1  12091  lemul2  12092  lemul2a  12094  lediv1  12104  gt0div  12105  ge0div  12106  mulsuble0b  12111  ltdivmul  12114  ledivmul  12115  ltdivmul2  12116  ledivmul2  12118  lemuldiv  12119  ltdiv23  12130  lediv23  12131  ledivp1i  12164  ltdivp1i  12165  uzind2  12714  nn0ind  12716  fnn0ind  12720  uz3m2nn  12943  xrltletr  13208  xrletr  13209  xrre2  13222  xrltmin  13234  xrlemin  13236  xleadd2a  13306  xleadd1  13307  xltadd2  13309  xmulasslem3  13338  xmulass  13339  xltmul2  13345  ixxdisj  13413  iooneg  13524  iccneg  13525  icoshft  13526  icoshftf1o  13527  icodisj  13529  snunioo  13531  fzen  13595  ssfzunsnext  13624  fzrev3  13645  2ffzeq  13704  fzoaddel2  13776  elfzodifsumelfzo  13787  ssfzoulel  13816  ssfzo12bi  13817  fzoopth  13818  fzoshftral  13843  adddivflid  13879  flltdivnn0lt  13894  ltdifltdiv  13895  fldiv4p1lem1div2  13896  modcyc  13967  modcyc2  13968  modaddabs  13972  muladdmod  13976  modsubmodmod  13994  modaddmodup  13998  modaddmulmod  14002  moddi  14003  modsubdir  14004  expdiv  14177  digit2  14300  nfile  14423  hashdifpr  14480  hashgt23el  14489  hashreshashfun  14504  hashf1dmcdm  14509  hash3tpexb  14559  fi1uzind  14572  ccatval1  14642  ccatass  14654  swrdval  14711  swrdnd  14724  swrd0  14728  swrdfv2  14731  pfxsuff1eqwrdeq  14768  swrdswrdlem  14773  pfxccatin12lem2a  14796  pfxccatin12lem1  14797  repswccat  14857  cshwidxmod  14874  cshwidxmodr  14875  cshf1  14881  repswcshw  14883  2cshw  14884  2cshwcom  14887  2cshwcshw  14896  cshwcsh2id  14899  ccatco  14906  2swrd2eqwrdeq  15026  wwlktovf  15029  brcnvtrclfv  15076  shftval2  15148  mulre  15208  absdiv  15382  absdiflt  15405  absdifle  15406  abs3dif  15419  cau3  15443  ello12r  15604  elo12r  15615  modfsummods  15880  geoisum1c  15969  rpnnen2lem4  16305  rpnnen2lem7  16308  addmulmodb  16355  dvdsmulc  16373  dvdsmulcr  16375  dvdsmultr1  16386  dvdsmultr2  16388  dvdssub2  16391  oexpneg  16435  divalgb  16494  ndvdsadd  16500  sadass  16561  modgcd  16622  dvdsgcd  16634  dvdsgcdb  16635  gcdass  16637  mulgcd  16638  absmulgcd  16639  rpmulgcd  16647  expgcd  16653  zexpgcd  16655  nn0seqcvgd  16660  algcvga  16669  lcmdvdsb  16703  lcmass  16704  lcmfunsnlem1  16727  lcmfunsnlem2lem1  16728  lcmfunsnlem2lem2  16729  coprmdvds  16743  coprmdvds2  16744  rpmul  16749  cncongr1  16757  cncongr2  16758  qnumdenbi  16835  modprm0  16897  coprimeprodsq  16900  pythagtriplem4  16911  pythagtriplem8  16915  pythagtriplem9  16916  pythagtriplem12  16918  pythagtriplem14  16920  pythagtriplem16  16922  pcpremul  16935  pcgcd  16970  vdwapval  17065  vdwapun  17066  prmgaplem3  17145  prmgaplem4  17146  prmgaplem7  17149  prmgapprmolem  17153  mreiincl  17680  mreincl  17683  mremre  17688  mrcss  17704  catcisolem  18199  pleval2  18423  pospo  18431  latlem  18525  latjcom  18535  latmcom  18551  lubss  18601  lubun  18603  clatglbss  18607  ipole  18622  ipolt  18623  pslem  18660  dirtr  18690  gsumsgrpccat  18949  gsumws2  18951  frmdmnd  18968  symggrplem  18993  isgrpi  19083  grpsubrcan  19144  grpinvsub  19145  grpsubeq0  19149  grpsubadd0sub  19150  grpnpcan  19155  qussub  19319  ghmsub  19351  symgpssefmnd  19523  symggrp  19527  symgextsymg  19551  gsmsymgreqlem2  19558  symgfixfolem1  19565  pmtrprfv3  19581  symggen  19597  lsmass  19796  efgsrel  19861  cntzcmn  19967  dvrcl  20545  unitdvcl  20546  dvrcan1  20550  subrngmre  20724  subrgmre  20759  rhmsubclem2  20848  rrgeq0  20862  abvsubtri  20993  abvtrivd  20998  lmodvsubval2  21101  rmodislmodlem  21113  rmodislmod  21114  lss0cl  21131  lssintcl  21148  lssincl  21149  reslmhm2  21237  lspvadd  21280  lspsntrim  21282  islbs3  21342  unichnlidl  21425  rnglidlmmgm  21442  cncrng  21606  xrsmcmn  21608  cndrng  21614  cnsrng  21619  absabv  21637  xrs1mnd  21653  psgnco  21796  zrhpsgninv  21798  zrhpsgnevpm  21804  zrhpsgnodpm  21805  zrhpsgnelbas  21807  zrhcopsgnelbas  21808  uvcresum  22006  lindfmm  22040  lindsmm  22041  evlsval2  22303  mamudm  22617  mamufacex  22618  matsubgcell  22656  matsc  22672  scmatscmide  22729  scmatrhmcl  22750  1marepvsma1  22805  m1detdiag  22819  mdetralt  22830  m2detleiblem7  22849  gsummatr01lem3  22879  gsummatr01  22881  smadiadetlem0  22883  decpmate  22991  decpmatcl  22992  pm2mpcl  23022  pm2mpghmlem2  23037  chfacfscmul0  23083  chfacfscmulgsum  23085  chfacfpmmul0  23087  chfacfpmmulgsum  23089  unopn  23128  clsss  23279  cldmre  23303  toponmre  23318  opnssneib  23340  restabs  23390  restcls  23406  restntr  23407  hausnei2  23578  cmpsublem  23624  bwth  23635  hausmapdom  23726  ptpjcn  23837  upxp  23849  ptrescn  23865  xkopjcn  23882  fbssfi  24063  snfil  24090  ufprim  24135  rnelfm  24179  flimrest  24209  fclsrest  24250  tmdgsum  24321  blpnfctr  24662  mscl  24687  xmscl  24688  xmsge0  24689  xmseq0  24690  restmetu  24796  ngpds  24830  tngngp3  24882  unitnmn0  24894  xrsxmet  25036  metds0  25077  mpomulcn  25095  cncfmptc  25140  isclmp  25325  cnlmod  25368  ncvsi  25379  cphsqrtcl  25412  cfil3i  25497  cfilres  25524  cmssmscld  25578  cmmbl  25762  voliunlem2  25779  itg2ub  25961  itgrecl  26025  r1pid  26386  eflogeq  26839  cxpadd  26916  cxpcom  26976  logbchbase  27008  relogbreexp  27012  relogbzexp  27013  relogbmulexp  27015  logbleb  27020  logblt  27021  lawcos  27053  pythag  27054  asinsinb  27134  acoscosb  27135  atantanb  27161  amgmlem  27226  lgsneg  27557  lgsne0  27571  lgsmodeq  27578  lgsmulsqcoprm  27579  gausslemma2dlem1a  27601  2sqreulem2  27688  ltsres  27898  noetainflem1  27973  ltlestr  27996  lestr  27998  nocvxmin  28020  madebdaylemold  28163  lrrecpo  28206  ltadds2im  28251  leadds1im  28252  leadds2im  28253  leadds1  28254  leadds2  28255  ltadds1  28257  addscan2  28258  addscan1  28259  subadds  28335  ltsubs1  28341  divscl  28488  oncutlt  28529  zsoring  28674  expscllem  28695  brbtwn2  29362  colinearalg  29367  eleesubd  29369  axcgrrflx  29371  axcgrtr  29372  axsegcon  29384  ax5seglem1  29385  ax5seglem2  29386  ax5seglem4  29389  axbtwnid  29396  axlowdimlem14  29412  axlowdim  29418  axcontlem5  29425  axcontlem7  29427  nb3grprlem2  29841  cplgr3v  29895  cusgrsizeindslem  29911  sizusglecusglem2  29922  umgr2v2e  29985  cusgrrusgr  30041  iswlk  30070  edginwlk  30094  uspgr2wlkeq  30105  uspgr2wlkeq2  30106  uspgr2wlkeqi  30107  wlkonprop  30116  wlkon2n0  30124  subgrwlk  30148  pthdadjvtx  30192  upgr2pthnlp  30197  spthonepeq  30217  pthdlem2lem  30232  crctcshwlkn0lem3  30280  crctcshwlkn0lem5  30282  wlkiswwlks2lem4  30340  wlkiswwlks2lem6  30342  wlklnwwlkln2lem  30350  wwlksnred  30360  wwlksnextbi  30362  wwlksnextwrd  30365  2pthdlem1  30398  2wlkdlem10  30403  umgr2adedgwlkonALT  30415  elwwlks2s3  30419  elwwlks2ons3im  30422  s3wwlks2on  30424  sps3wwlks2on  30425  2wspdisj  30433  2wspiundisj  30434  clwwlkgt0  30456  clwlkclwwlklem2a4  30467  clwlkclwwlklem2a  30468  clwlkclwwlk  30472  clwlkclwwlk2  30473  clwlkclwwlkfo  30479  clwwisshclwwslemlem  30483  erclwwlktr  30492  clwwlkf  30517  wwlksubclwwlk  30528  erclwwlkntr  30541  clwwlknon  30560  frcond1  30746  frgr3v  30755  3vfriswmgr  30758  frgrwopreglem4a  30790  frrusgrord0lem  30819  clwwnonrepclwwnon  30825  extwwlkfab  30832  numclwwlk1lem2f1  30837  numclwwlk1lem2fo  30838  clwlknon2num  30848  numclwwlk2lem1  30856  numclwlk2lem2f  30857  numclwlk2lem2f1o  30859  numclwwlk2  30861  frgrreggt1  30873  friendshipgt3  30878  imsmetlem  31171  nmoxr  31247  nmoolb  31252  blometi  31284  phpar2  31304  phpar  31305  ipasslem5  31316  hvadd32  31515  hvaddsub12  31519  hvaddsubass  31522  hvsubass  31525  hvsub32  31526  hvsubdistr1  31530  hvsubdistr2  31531  hvmulcan  31553  hvmulcan2  31554  hvsubcan  31555  his5  31567  his2sub  31573  hhssabloilem  31742  hhssnv  31745  shlej2  31842  pjoi0  32198  hodcl  32228  hoadd32  32264  hosubdi  32289  hosubsub2  32293  hoaddsubass  32296  hosubsub4  32299  nmoplb  32388  unop  32396  hmop  32403  nmfnlb  32405  lnopmul  32448  kbass1  32597  kbass2  32598  leopmul2i  32616  leoptr  32618  cvntr  32773  mdslmd4i  32814  mdexchi  32816  atcv1  32861  sumdmdii  32896  fcoinvbr  33078  fpwrelmapffs  33205  xreceu  33367  isinftm  33621  inlidl  33849  unitdivcld  34411  esummulc1  34591  hasheuni  34595  unelsiga  34644  inelpisys  34665  carsgsigalem  34826  signswmnd  35065  bnj545  35404  bnj594  35421  bnj1311  35533  fissorduni  35594  r1filimi  35611  fineqvac  35642  fineqvnttrclselem3  35649  fineqvinfep  35651  usgrgt2cycl  35723  acycgr1v  35728  cvmsf1o  35851  cvmscld  35852  satefvfmla1  36004  elnanelprv  36008  lediv2aALT  36256  gcd32  36328  fununiq  36348  dfrdg4  36530  brcolinear  36639  colinearex  36640  ltnmul  36796  ltnadd  36798  nn0prpwlem  36941  clsun  36947  fnemeet1  36985  fnemeet2  36986  fnejoin1  36987  fnejoin2  36988  eltail  36993  rdgeqoa  38124  nlpineqsn  38162  lindsadd  38367  poimirlem28  38397  cnambfre  38417  ftc1anclem4  38445  cocanfo  38469  f1ocan1fv  38476  metf1o  38505  ismtybnd  38557  ghomco  38641  isdrngo2  38708  inidl  38780  igenmin  38814  brxrn  39131  brredunds  39458  cmtvalN  40084  cvrval  40142  pmapmeet  40646  paddval  40671  paddssat  40687  elpcliN  40766  pclssN  40767  pclunN  40771  paddunN  40800  poldmj1N  40801  tendoplcl2  41651  tendoplcl  41654  dihmeet  42216  lcmineqlem1  42895  reltsub1  43261  reltsubadd2  43262  resubsub4  43264  reppncan  43268  resubdi  43271  readdcan2  43288  subresre  43306  mapco2g  43559  mzpcompact2lem  43596  eqrabdioph  43622  lerabdioph  43646  eluzrabdioph  43647  ltrabdioph  43649  nerabdioph  43650  dvdsrabdioph  43651  reglogcl  43731  rmxyadd  43762  rmyabs  43799  congadd  43807  congabseq  43815  rmydioph  43855  mendring  44029  mendlmod  44030  iocinico  44053  omge1  44138  relexp0a  44556  relexpaddss  44558  brcoffn  44870  ismnushort  45125  dvconstbi  45158  uzwo4  45887  ssin0  45889  ssinc  45919  ssdec  45920  fvmpt2bd  46002  disjf1o  46023  ssnnf1octb  46026  sub31  46123  fperiodmullem  46136  ssfiunibd  46142  infxr  46196  fmul01  46410  islptre  46449  lptre2pt  46468  limcleqr  46472  limclner  46479  limsuppnflem  46538  limsupvaluz2  46566  supcnvlimsup  46568  xlimmnfvlem2  46661  xlimmnfv  46662  xlimpnfvlem2  46665  xlimpnfv  46666  climxlim2lem  46673  coskpi2  46694  cosknegpi  46697  dvnmptdivc  46766  dvdsn1add  46767  dvnmptconst  46769  dvmptfprod  46773  dvnprodlem1  46774  dvnprodlem2  46775  ovolsplit  46816  stoweidlem60  46888  stowei  46892  dirkeritg  46930  fourierdlem70  47004  fourierdlem71  47005  fourierdlem103  47037  fourierdlem104  47038  fouriersw  47059  rrxtopnfi  47115  saluncl  47145  salexct  47162  sge0ltfirp  47228  sge0iunmpt  47246  meadjiunlem  47293  meaiuninc3v  47312  carageniuncllem1  47349  caratheodorylem1  47354  ovncvrrp  47392  ovnsubaddlem1  47398  hspmbllem2  47455  ovolval5lem3  47482  smfpimbor1lem1  47626  smfsuplem1  47639  smflimsuplem4  47651  sigarls  47685  cnambpcma  48182  elfzelfzlble  48209  submodaddmod  48235  difltmodne  48236  m1mod0mod1  48248  modmkpkne  48255  mod2addne  48258  modm2nep1  48260  modm1nep2  48262  modm1nem2  48263  fsumsplitsndif  48269  fundcmpsurinjALT  48312  iccpartiltu  48322  prproropf1olem2  48404  fmtno4prmfac  48475  2pwp1prmfmtno  48493  lighneallem4b  48512  nprmdvdsfacm1lem4  48526  mogoldbblem  48636  gbegt5  48677  sbgoldbm  48700  nnsum3primesle9  48710  nnsum4primesodd  48712  nnsum4primesoddALTV  48713  evengpoap3  48715  nnsum4primesevenALTV  48717  clnbgredg  48756  opstrgric  48842  clnbgrgrimlem  48849  grtrif1o  48858  isubgr3stgrlem1  48882  isubgr3stgrlem4  48885  gpgusgralem  48972  gpg3nbgrvtx0  48992  isupwlk  49052  lidldomnnring  49151  2zrngacmnd  49163  rhmsubcALTVlem2  49197  fprmappr  49275  zlmodzxzscm  49287  gsumlsscl  49310  lincvalsng  49346  lincvalpr  49348  lincdifsn  49354  linc1  49355  lincellss  49356  fdivmpt  49470  digexp  49537  2arymaptfo  49584  line  49662  rrxline  49664  itsclc0xyqsolr  49699  iscnrm3r  49874  resipos  49901  amgmwlem  50820