Theorem 3adant1 1128

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  3ad2ant2  1132  3ad2ant3  1133  3simpc  1148  eupickb  2637  spc3egv  3532  sbciegft  3749  reuhyp  5338  predtrss  6214  funopg  6452  funprg  6472  funtpg  6473  funcnvtp  6481  unima  6825  fvun1  6841  fnreseql  6907  xpprsng  6994  ftpg  7010  f13dfv  7127  f1ofvswap  7158  mpoeq3ia  7331  ordunel  7649  fex2  7754  funexw  7768  poxp  7940  suppval1  7954  wfr3g  8109  smores3  8155  oaord  8340  oacan  8341  oaword  8342  omord  8361  omcan  8362  omwordri  8365  odi  8372  omass  8373  oeord  8381  oecan  8382  oewordri  8385  oeordsuc  8387  nnaord  8412  nnaordr  8413  nndi  8416  nnmass  8417  nnaword  8420  nnmord  8425  nnmwordri  8429  erov  8561  ecopovtrn  8567  ixpf  8666  mapxpen  8879  dif1enlem  8905  ssfi  8918  sbthfilem  8941  sbthfi  8942  fimax2g  8990  unbnn  9000  funisfsupp  9063  inelfi  9107  elfiun  9119  sup0  9155  suppr  9160  infpr  9192  trpredpo  9414  frr3g  9445  r111  9464  dif1card  9697  ackbij1lem16  9922  cff1  9945  cfflb  9946  cfsmolem  9957  fin23lem34  10033  hsmexlem2  10114  axcc3  10125  domtriomlem  10129  axdc3lem4  10140  axdc4lem  10142  axcclem  10144  konigthlem  10255  gchdomtri  10316  tskpr  10457  tskop  10458  tskuni  10470  tskun  10473  gruop  10492  gruun  10493  grudomon  10504  adderpqlem  10641  mulerpqlem  10642  addassnq  10645  mulassnq  10646  distrnq  10648  ltsonq  10656  ltanq  10658  ltmnq  10659  genpass  10696  distrlem1pr  10712  distrlem4pr  10713  ltsopr  10719  adddir  10897  axlttrn  10978  ltletr  10997  letr  10999  mul32  11071  mul31  11072  add32  11123  subsub23  11156  addsubass  11161  subcan2  11176  subsub2  11179  nppcan2  11182  sub32  11185  nnncan  11186  nnncan2  11188  pnpcan2  11191  subdi  11338  subdir  11339  receu  11550  mulcan1g  11558  mulcan2g  11559  divmul3  11568  divrec  11579  divrec2  11580  divsubdir  11599  subdivcomb2  11601  divdiv1  11616  redivcl  11624  div2neg  11628  ltmul2  11756  lemul1  11757  lemul2  11758  lemul2a  11760  lediv1  11770  gt0div  11771  ge0div  11772  mulsuble0b  11777  ltdivmul  11780  ledivmul  11781  ltdivmul2  11782  ledivmul2  11784  lemuldiv  11785  ltdiv23  11796  lediv23  11797  ledivp1i  11830  ltdivp1i  11831  uzind2  12343  nn0ind  12345  fnn0ind  12349  uz3m2nn  12560  xrltletr  12820  xrletr  12821  xrre2  12833  xrltmin  12845  xrlemin  12847  xleadd2a  12917  xleadd1  12918  xltadd2  12920  xmulasslem3  12949  xmulass  12950  xltmul2  12956  ixxdisj  13023  iooneg  13132  iccneg  13133  icoshft  13134  icoshftf1o  13135  icodisj  13137  snunioo  13139  fzen  13202  ssfzunsnext  13230  fzrev3  13251  2ffzeq  13306  fzoaddel2  13371  elfzodifsumelfzo  13381  ssfzoulel  13409  ssfzo12bi  13410  fzoshftral  13432  adddivflid  13466  flltdivnn0lt  13481  ltdifltdiv  13482  fldiv4p1lem1div2  13483  modcyc  13554  modcyc2  13555  modaddabs  13557  modsubmodmod  13578  modaddmodup  13582  modaddmulmod  13586  moddi  13587  modsubdir  13588  expdiv  13762  digit2  13879  nfile  14002  hashdifpr  14058  hashgt23el  14067  hashreshashfun  14082  fi1uzind  14139  ccatval1  14209  ccatass  14221  swrdval  14284  swrdnd  14295  swrd0  14299  swrdfv2  14302  pfxsuff1eqwrdeq  14340  swrdswrdlem  14345  pfxccatin12lem2a  14368  pfxccatin12lem1  14369  repswccat  14427  cshwidxmod  14444  cshwidxmodr  14445  cshf1  14451  repswcshw  14453  2cshw  14454  2cshwcom  14457  2cshwcshw  14466  cshwcsh2id  14469  ccatco  14476  2swrd2eqwrdeq  14594  wwlktovf  14599  brcnvtrclfv  14642  shftval2  14714  mulre  14760  absdiv  14935  absdiflt  14957  absdifle  14958  abs3dif  14971  cau3  14995  ello12r  15154  elo12r  15165  modfsummods  15433  geoisum1c  15520  rpnnen2lem4  15854  rpnnen2lem7  15857  dvdsmulc  15921  dvdsmulcr  15923  dvdsmultr1  15933  dvdsmultr2  15935  dvdssub2  15938  oexpneg  15982  divalgb  16041  ndvdsadd  16047  sadass  16106  modgcd  16168  dvdsgcd  16180  dvdsgcdb  16181  gcdass  16183  mulgcd  16184  absmulgcd  16185  rpmulgcd  16194  nn0seqcvgd  16203  algcvga  16212  lcmdvdsb  16246  lcmass  16247  lcmfunsnlem1  16270  lcmfunsnlem2lem1  16271  lcmfunsnlem2lem2  16272  coprmdvds  16286  coprmdvds2  16287  rpmul  16292  cncongr1  16300  cncongr2  16301  qnumdenbi  16376  modprm0  16434  coprimeprodsq  16437  pythagtriplem4  16448  pythagtriplem8  16452  pythagtriplem9  16453  pythagtriplem12  16455  pythagtriplem14  16457  pythagtriplem16  16459  pcpremul  16472  pcgcd  16507  vdwapval  16602  vdwapun  16603  prmgaplem3  16682  prmgaplem4  16683  prmgaplem7  16686  prmgapprmolem  16690  mreiincl  17222  mreincl  17225  mremre  17230  mrcss  17242  catcisolem  17741  pleval2  17970  pospo  17978  latlem  18070  latjcom  18080  latmcom  18096  lubss  18146  lubun  18148  clatglbss  18152  ipole  18167  ipolt  18168  pslem  18205  dirtr  18235  gsumsgrpccat  18393  gsumws2  18396  frmdmnd  18413  symggrplem  18438  isgrpi  18517  grpsubrcan  18571  grpinvsub  18572  grpsubeq0  18576  grpsubadd0sub  18577  grpnpcan  18582  qussub  18731  ghmsub  18757  symgpssefmnd  18918  symggrp  18923  symgextsymg  18947  gsmsymgreqlem2  18954  symgfixfolem1  18961  pmtrprfv3  18977  symggen  18993  lsmass  19190  efgsrel  19255  cntzcmn  19356  dvrcl  19843  unitdvcl  19844  dvrcan1  19848  subrgmre  19963  abvsubtri  20010  abvtrivd  20015  lmodvsubval2  20093  rmodislmodlem  20105  rmodislmod  20106  rmodislmodOLD  20107  lss0cl  20123  lssintcl  20141  lssincl  20142  reslmhm2  20230  lspvadd  20273  lspsntrim  20275  islbs3  20332  rrgeq0  20474  cncrng  20531  xrsmcmn  20533  cndrng  20539  cnsrng  20544  xrs1mnd  20548  absabv  20567  psgnco  20700  zrhpsgninv  20702  zrhpsgnevpm  20708  zrhpsgnodpm  20709  zrhpsgnelbas  20711  zrhcopsgnelbas  20712  uvcresum  20910  lindfmm  20944  lindsmm  20945  evlsval2  21207  mamudm  21447  mamufacex  21448  matsubgcell  21491  matsc  21507  scmatscmide  21564  scmatrhmcl  21585  1marepvsma1  21640  m1detdiag  21654  mdetralt  21665  m2detleiblem7  21684  gsummatr01lem3  21714  gsummatr01  21716  smadiadetlem0  21718  decpmate  21823  decpmatcl  21824  pm2mpcl  21854  pm2mpghmlem2  21869  chfacfscmul0  21915  chfacfscmulgsum  21917  chfacfpmmul0  21919  chfacfpmmulgsum  21921  unopn  21960  clsss  22113  cldmre  22137  toponmre  22152  opnssneib  22174  restabs  22224  restcls  22240  restntr  22241  hausnei2  22412  cmpsublem  22458  bwth  22469  hausmapdom  22559  ptpjcn  22670  upxp  22682  ptrescn  22698  xkopjcn  22715  fbssfi  22896  snfil  22923  ufprim  22968  rnelfm  23012  flimrest  23042  fclsrest  23083  tmdgsum  23154  blpnfctr  23497  mscl  23522  xmscl  23523  xmsge0  23524  xmseq0  23525  restmetu  23632  ngpds  23666  tngngp3  23726  unitnmn0  23738  xrsxmet  23878  metds0  23919  cncfmptc  23981  isclmp  24166  cnlmod  24209  ncvsi  24220  cphsqrtcl  24253  cfil3i  24338  cfilres  24365  cmssmscld  24419  cmmbl  24603  voliunlem2  24620  itg2ub  24803  itgrecl  24867  tdeglem3OLD  25128  r1pid  25229  eflogeq  25662  cxpadd  25739  cxpcom  25797  logbchbase  25826  relogbreexp  25830  relogbzexp  25831  relogbmulexp  25833  logbleb  25838  logblt  25839  lawcos  25871  pythag  25872  asinsinb  25952  acoscosb  25953  atantanb  25979  amgmlem  26044  lgsneg  26374  lgsne0  26388  lgsmodeq  26395  lgsmulsqcoprm  26396  gausslemma2dlem1a  26418  2sqreulem2  26505  brbtwn2  27176  colinearalg  27181  eleesubd  27183  axcgrrflx  27185  axcgrtr  27186  axsegcon  27198  ax5seglem1  27199  ax5seglem2  27200  ax5seglem4  27203  axbtwnid  27210  axlowdimlem14  27226  axlowdim  27232  axcontlem5  27239  axcontlem7  27241  nb3grprlem2  27651  cplgr3v  27705  cusgrsizeindslem  27721  sizusglecusglem2  27732  umgr2v2e  27795  cusgrrusgr  27851  iswlk  27880  edginwlk  27904  uspgr2wlkeq  27915  uspgr2wlkeq2  27916  uspgr2wlkeqi  27917  wlkonprop  27928  wlkon2n0  27936  pthdadjvtx  27999  upgr2pthnlp  28001  spthonepeq  28021  pthdlem2lem  28036  crctcshwlkn0lem3  28078  crctcshwlkn0lem5  28080  wlkiswwlks2lem4  28138  wlkiswwlks2lem6  28140  wlklnwwlkln2lem  28148  wwlksnred  28158  wwlksnextbi  28160  wwlksnextwrd  28163  2pthdlem1  28196  2wlkdlem10  28201  umgr2adedgwlkonALT  28213  elwwlks2s3  28217  elwwlks2ons3im  28220  s3wwlks2on  28222  2wspdisj  28228  2wspiundisj  28229  clwwlkgt0  28251  clwlkclwwlklem2a4  28262  clwlkclwwlklem2a  28263  clwlkclwwlk  28267  clwlkclwwlk2  28268  clwlkclwwlkfo  28274  clwwisshclwwslemlem  28278  erclwwlktr  28287  clwwlkf  28312  wwlksubclwwlk  28323  erclwwlkntr  28336  clwwlknon  28355  frcond1  28531  frgr3v  28540  3vfriswmgr  28543  frgrwopreglem4a  28575  frrusgrord0lem  28604  clwwnonrepclwwnon  28610  extwwlkfab  28617  numclwwlk1lem2f1  28622  numclwwlk1lem2fo  28623  clwlknon2num  28633  numclwwlk2lem1  28641  numclwlk2lem2f  28642  numclwlk2lem2f1o  28644  numclwwlk2  28646  frgrreggt1  28658  friendshipgt3  28663  imsmetlem  28953  nmoxr  29029  nmoolb  29034  blometi  29066  phpar2  29086  phpar  29087  ipasslem5  29098  hvadd32  29297  hvaddsub12  29301  hvaddsubass  29304  hvsubass  29307  hvsub32  29308  hvsubdistr1  29312  hvsubdistr2  29313  hvmulcan  29335  hvmulcan2  29336  hvsubcan  29337  his5  29349  his2sub  29355  hhssabloilem  29524  hhssnv  29527  shlej2  29624  pjoi0  29980  hodcl  30010  hoadd32  30046  hosubdi  30071  hosubsub2  30075  hoaddsubass  30078  hosubsub4  30081  nmoplb  30170  unop  30178  hmop  30185  nmfnlb  30187  lnopmul  30230  kbass1  30379  kbass2  30380  leopmul2i  30398  leoptr  30400  cvntr  30555  mdslmd4i  30596  mdexchi  30598  atcv1  30643  sumdmdii  30678  fcoinvbr  30848  fpwrelmapffs  30971  xreceu  31098  isinftm  31337  unitdivcld  31753  esummulc1  31949  hasheuni  31953  unelsiga  32002  inelpisys  32022  carsgsigalem  32182  signswmnd  32436  bnj545  32775  bnj594  32792  bnj1311  32904  fineqvac  32966  hashf1dmcdm  32976  usgrgt2cycl  32992  subgrwlk  32994  acycgr1v  33011  cvmsf1o  33134  cvmscld  33135  satefvfmla1  33287  elnanelprv  33291  lediv2aALT  33535  onunel  33592  gcd32  33621  fununiq  33649  ttrclss  33706  poxp2  33717  poxp3  33723  poseq  33729  naddelim  33765  naddel1  33766  naddel2  33767  naddss1  33768  naddss2  33769  sltres  33792  noetainflem1  33867  sltletr  33886  sletr  33888  nocvxmin  33900  madebdaylemold  34005  lrrecpo  34025  dfrdg4  34180  brcolinear  34288  colinearex  34289  nn0prpwlem  34438  clsun  34444  fnemeet1  34482  fnemeet2  34483  fnejoin1  34484  fnejoin2  34485  eltail  34490  rdgeqoa  35468  nlpineqsn  35506  curf  35682  lindsadd  35697  poimirlem28  35732  cnambfre  35752  ftc1anclem4  35780  cocanfo  35803  f1ocan1fv  35811  metf1o  35840  ismtybnd  35892  ghomco  35976  isdrngo2  36043  inidl  36115  igenmin  36149  brxrn  36431  brredunds  36666  cmtvalN  37152  cvrval  37210  pmapmeet  37714  paddval  37739  paddssat  37755  elpcliN  37834  pclssN  37835  pclunN  37839  paddunN  37868  poldmj1N  37869  tendoplcl2  38719  tendoplcl  38722  dihmeet  39284  lcmineqlem1  39965  factwoffsmonot  40091  expgcd  40255  zexpgcd  40257  reltsub1  40290  reltsubadd2  40291  resubsub4  40293  reppncan  40297  resubdi  40300  readdcan2  40316  subresre  40333  mapco2g  40452  mzpcompact2lem  40489  eqrabdioph  40515  lerabdioph  40543  eluzrabdioph  40544  ltrabdioph  40546  nerabdioph  40547  dvdsrabdioph  40548  reglogcl  40628  rmxyadd  40659  rmyabs  40696  congadd  40704  congabseq  40712  rmydioph  40752  mendring  40933  mendlmod  40934  iocinico  40959  relexp0a  41213  relexpaddss  41215  brcoffn  41529  ismnushort  41808  dvconstbi  41841  uzwo4  42490  ssin0  42492  ssinc  42526  ssdec  42527  fvmpt2bd  42595  disjf1o  42618  ssnnf1octb  42622  sub31  42719  fperiodmullem  42732  ssfiunibd  42738  infxr  42796  fmul01  43011  islptre  43050  lptre2pt  43071  limcleqr  43075  limclner  43082  limsuppnflem  43141  limsupvaluz2  43169  supcnvlimsup  43171  xlimmnfvlem2  43264  xlimmnfv  43265  xlimpnfvlem2  43268  xlimpnfv  43269  climxlim2lem  43276  coskpi2  43297  cosknegpi  43300  dvnmptdivc  43369  dvdsn1add  43370  dvnmptconst  43372  dvmptfprod  43376  dvnprodlem1  43377  dvnprodlem2  43378  ovolsplit  43419  stoweidlem60  43491  stowei  43495  dirkeritg  43533  fourierdlem70  43607  fourierdlem71  43608  fourierdlem103  43640  fourierdlem104  43641  fouriersw  43662  rrxtopnfi  43718  saluncl  43748  salexct  43763  sge0ltfirp  43828  sge0iunmpt  43846  meadjiunlem  43893  meaiuninc3v  43912  carageniuncllem1  43949  caratheodorylem1  43954  ovncvrrp  43992  ovnsubaddlem1  43998  hspmbllem2  44055  ovolval5lem3  44082  smfpimbor1lem1  44219  smfsuplem1  44231  smflimsuplem4  44243  sigarls  44260  cnambpcma  44674  elfzelfzlble  44701  fzoopth  44707  m1mod0mod1  44709  fsumsplitsndif  44713  fundcmpsurinjALT  44752  iccpartiltu  44762  prproropf1olem2  44844  fmtno4prmfac  44912  2pwp1prmfmtno  44930  lighneallem4b  44949  mogoldbblem  45060  gbegt5  45101  sbgoldbm  45124  nnsum3primesle9  45134  nnsum4primesodd  45136  nnsum4primesoddALTV  45137  evengpoap3  45139  nnsum4primesevenALTV  45141  isomgrtr  45179  strisomgrop  45180  isupwlk  45186  lidldomnnring  45376  2zrngacmnd  45388  rhmsubclem2  45533  rhmsubcALTVlem2  45551  fprmappr  45569  zlmodzxzscm  45581  gsumlsscl  45607  lincvalsng  45645  lincvalpr  45647  lincdifsn  45653  linc1  45654  lincellss  45655  difmodm1lt  45756  fdivmpt  45774  digexp  45841  2arymaptfo  45888  line  45966  rrxline  45968  itsclc0xyqsolr  46003  iscnrm3r  46130  amgmwlem  46392