Theorem 3adant1 1079

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.)

Hypothesis

Ref	Expression
3adant.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
3adant1	⊢ ((𝜃 ∧ 𝜑 ∧ 𝜓) → 𝜒)

Proof of Theorem 3adant1

Step	Hyp	Ref	Expression
1		3simpc 1060	. 2 ⊢ ((𝜃 ∧ 𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜓))
2		3adant.1	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3	1, 2	syl 17	1 ⊢ ((𝜃 ∧ 𝜑 ∧ 𝜓) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  3ad2ant2  1083  3ad2ant3  1084  eupickb  2538  sbciegft  3466  reuhyp  4896  funopg  5922  funprg  5940  funtpg  5942  funcnvtp  5951  fvun1  6269  fnreseql  6327  ftpg  6423  f13dfv  6530  mpt2eq3ia  6720  ordunel  7027  fex2  7121  poxp  7289  suppval1  7301  wfr3g  7413  smores3  7450  oaord  7627  oacan  7628  oaword  7629  omord  7648  omcan  7649  omwordri  7652  odi  7659  omass  7660  oeord  7668  oecan  7669  oewordri  7672  oeordsuc  7674  nnaord  7699  nnaordr  7700  nndi  7703  nnmass  7704  nnaword  7707  nnmord  7712  nnmwordri  7716  erov  7844  ecopovtrn  7850  ixpf  7930  mapxpen  8126  fimax2g  8206  unbnn  8216  funisfsupp  8280  inelfi  8324  elfiun  8336  sup0  8372  suppr  8377  infpr  8409  r111  8638  dif1card  8833  xpcdaen  9005  mapcdaen  9006  ackbij1lem16  9057  cff1  9080  cfflb  9081  cfsmolem  9092  fin23lem34  9168  hsmexlem2  9249  axcc3  9260  domtriomlem  9264  axdc3lem4  9275  axdc4lem  9277  axcclem  9279  konigthlem  9390  gchdomtri  9451  tskpr  9592  tskop  9593  tskuni  9605  tskun  9608  gruop  9627  gruun  9628  grudomon  9639  adderpqlem  9776  mulerpqlem  9777  addassnq  9780  mulassnq  9781  distrnq  9783  ltsonq  9791  ltanq  9793  ltmnq  9794  genpass  9831  distrlem1pr  9847  distrlem4pr  9848  ltsopr  9854  adddir  10031  axlttrn  10110  ltletr  10129  letr  10131  mul32  10203  mul31  10204  add32  10254  subsub23  10286  addsubass  10291  subcan2  10306  subsub2  10309  nppcan2  10312  sub32  10315  nnncan  10316  nnncan2  10318  pnpcan2  10321  subdi  10463  subdir  10464  receu  10672  mulcan1g  10680  mulcan2g  10681  divmul3  10690  divrec  10701  divrec2  10702  divsubdir  10721  divdiv1  10736  redivcl  10744  div2neg  10748  ltmul2  10874  lemul1  10875  lemul2  10876  lemul2a  10878  lediv1  10888  gt0div  10889  ge0div  10890  mulsuble0b  10895  ltdivmul  10898  ledivmul  10899  ltdivmul2  10900  ledivmul2  10902  lemuldiv  10903  ltdiv23  10914  lediv23  10915  ledivp1i  10949  ltdivp1i  10950  uzind2  11470  nn0ind  11472  fnn0ind  11476  uz3m2nn  11731  xrltletr  11988  xrletr  11989  xrre2  12001  xrltmin  12013  xrlemin  12015  xleadd2a  12084  xleadd1  12085  xltadd2  12087  xmulasslem3  12116  xmulass  12117  xltmul2  12123  ixxdisj  12190  iooneg  12292  iccneg  12293  icoshft  12294  icoshftf1o  12295  icodisj  12297  snunioo  12298  fzen  12358  ssfzunsnext  12386  fzrev3  12406  2ffzeq  12460  fzoaddel2  12523  elfzodifsumelfzo  12533  ssfzoulel  12562  ssfzo12bi  12563  fzoshftral  12585  adddivflid  12619  flltdivnn0lt  12634  ltdifltdiv  12635  fldiv4p1lem1div2  12636  modcyc  12705  modcyc2  12706  modaddabs  12708  modsubmodmod  12729  modaddmodup  12733  modaddmulmod  12737  moddi  12738  modsubdir  12739  expdiv  12911  digit2  12997  nfile  13150  hashdifpr  13203  hashreshashfun  13226  fi1uzind  13279  fi1uzindOLD  13285  ccatass  13371  lswccatn0lsw  13373  swrdval  13417  swrdnd  13432  swrd0  13434  swrdfv2  13446  2swrd1eqwrdeq  13454  swrdswrdlem  13459  swrdccatin12lem2a  13485  swrdccatin12lem2b  13486  repswccat  13532  cshwidxmod  13549  cshwidxmodr  13550  cshf1  13556  repswcshw  13558  2cshw  13559  2cshwcom  13562  2cshwcshw  13571  cshwcsh2id  13574  ccatco  13581  2swrd2eqwrdeq  13696  wwlktovf  13699  brcnvtrclfv  13744  shftval2  13815  mulre  13861  absdiv  14035  absdiflt  14057  absdifle  14058  abs3dif  14071  cau3  14095  ello12r  14248  elo12r  14259  modfsummods  14525  geoisum1c  14611  rpnnen2lem4  14946  rpnnen2lem7  14949  dvdsmulc  15009  dvdsmulcr  15011  dvdsmultr1  15019  dvdsmultr2  15021  dvdssub2  15023  oexpneg  15069  divalgb  15127  ndvdsadd  15134  sadass  15193  modgcd  15253  dvdsgcd  15261  dvdsgcdb  15262  gcdass  15264  mulgcd  15265  absmulgcd  15266  rpmulgcd  15275  nn0seqcvgd  15283  algcvga  15292  lcmdvdsb  15326  lcmass  15327  lcmfunsnlem1  15350  lcmfunsnlem2lem1  15351  lcmfunsnlem2lem2  15352  coprmdvds  15366  coprmdvdsOLD  15367  coprmdvds2  15368  rpmul  15373  cncongr1  15381  cncongr2  15382  prmgt1  15409  qnumdenbi  15452  modprm0  15510  coprimeprodsq  15513  pythagtriplem4  15524  pythagtriplem8  15528  pythagtriplem9  15529  pythagtriplem12  15531  pythagtriplem14  15533  pythagtriplem16  15535  pcpremul  15548  pcgcd  15582  vdwapval  15677  vdwapun  15678  prmgaplem3  15757  prmgaplem4  15758  prmgaplem7  15761  prmgapprmolem  15765  setsstructOLD  15899  mreiincl  16256  mreincl  16259  mremre  16264  mrcss  16276  catcisolem  16756  pleval2  16965  pospo  16973  latlem  17049  latjcom  17059  latmcom  17075  lubss  17121  lubun  17123  clatglbss  17127  ipole  17158  ipolt  17159  pslem  17206  dirtr  17236  gsumws2  17379  frmdmnd  17396  isgrpi  17445  grpsubrcan  17496  grpinvsub  17497  grpsubeq0  17501  grpsubadd0sub  17502  grpnpcan  17507  qussub  17654  ghmsub  17668  symggrp  17820  symgextsymg  17844  gsmsymgreqlem2  17851  symgfixfolem1  17858  pmtrprfv3  17874  symggen  17890  lsmass  18083  efgsrel  18147  cntzcmn  18245  dvrcl  18686  unitdvcl  18687  dvrcan1  18691  subrgmre  18804  abvsubtri  18835  abvtrivd  18840  lmodvsubval2  18918  rmodislmodlem  18930  rmodislmod  18931  lss0cl  18947  lssintcl  18964  lssincl  18965  reslmhm2  19053  lspvadd  19096  lspsntrim  19098  islbs3  19155  rrgeq0  19290  evlsval2  19520  cncrng  19767  xrsmcmn  19769  cndrng  19775  cnsrng  19780  xrs1mnd  19784  absabv  19803  psgnco  19929  zrhpsgninv  19931  zrhpsgnevpm  19937  zrhpsgnodpm  19938  zrhpsgnelbas  19940  zrhcopsgnelbas  19941  uvcresum  20132  lindfmm  20166  lindsmm  20167  mamudm  20194  mamufacex  20195  matsubgcell  20240  matsc  20256  scmatscmide  20313  scmatrhmcl  20334  1marepvsma1  20389  m1detdiag  20403  mdetralt  20414  m2detleiblem7  20433  gsummatr01lem3  20463  gsummatr01  20465  smadiadetlem0  20467  decpmate  20571  decpmatcl  20572  pm2mpcl  20602  pm2mpghmlem2  20617  chfacfscmul0  20663  chfacfscmulgsum  20665  chfacfpmmul0  20667  chfacfpmmulgsum  20669  unopn  20708  clsss  20858  cldmre  20882  toponmre  20897  opnssneib  20919  restabs  20969  restcls  20985  restntr  20986  hausnei2  21157  cmpsublem  21202  bwth  21213  hausmapdom  21303  ptpjcn  21414  upxp  21426  ptrescn  21442  xkopjcn  21459  fbssfi  21641  snfil  21668  ufprim  21713  rnelfm  21757  flimrest  21787  fclsrest  21828  tmdgsum  21899  blpnfctr  22241  mscl  22266  xmscl  22267  xmsge0  22268  xmseq0  22269  restmetu  22375  ngpds  22408  tngngp3  22460  unitnmn0  22472  xrsxmet  22612  metds0  22653  cncfmptc  22714  isclmp  22897  cnlmod  22940  ncvsi  22951  cphsqrtcl  22984  cfil3i  23067  cfilres  23094  cmmbl  23302  voliunlem2  23319  itg2ub  23500  itgrecl  23564  tdeglem3  23819  r1pid  23919  eflogeq  24348  cxpadd  24425  logbchbase  24509  relogbreexp  24513  relogbzexp  24514  relogbmulexp  24516  logbleb  24521  logblt  24522  lawcos  24546  pythag  24547  asinsinb  24624  acoscosb  24625  atantanb  24651  amgmlem  24716  lgsneg  25046  lgsne0  25060  lgsmodeq  25067  lgsmulsqcoprm  25068  gausslemma2dlem1a  25090  brbtwn2  25785  colinearalg  25790  eleesubd  25792  axcgrrflx  25794  axcgrtr  25795  axsegcon  25807  ax5seglem1  25808  ax5seglem2  25809  ax5seglem4  25812  axbtwnid  25819  axlowdimlem14  25835  axlowdim  25841  axcontlem5  25848  axcontlem7  25850  funvtxdmge2valOLD  25899  funiedgdmge2valOLD  25900  usgr1v0e  26218  nb3grprlem2  26283  cplgr3v  26331  cusgrsizeindslem  26347  sizusglecusglem2  26358  umgr2v2e  26421  cusgrrusgr  26477  iswlk  26506  edginwlk  26530  uspgr2wlkeq  26542  uspgr2wlkeq2  26543  uspgr2wlkeqi  26544  wlkon2n0  26562  pthdadjvtx  26626  upgr2pthnlp  26628  spthonepeq  26648  pthdlem2lem  26663  crctcshwlkn0lem3  26704  crctcshwlkn0lem5  26706  wlkiswwlks2lem4  26758  wlkiswwlks2lem6  26760  wlklnwwlkln2lem  26768  wwlksnred  26787  wwlksnextbi  26789  wwlksnextwrd  26792  2pthdlem1  26826  2wlkdlem10  26831  umgr2adedgwlkonALT  26843  elwwlks2ons3  26848  s3wwlks2on  26849  elwspths2on  26853  2wspdisj  26855  2wspiundisj  26856  clwwlknp  26887  isclwwlksng  26888  clwlkclwwlklem2a4  26898  clwlkclwwlklem2a  26899  clwlkclwwlk  26903  clwlkclwwlk2  26904  clwwlksgt0  26906  clwwlksf  26915  wwlksubclwwlks  26925  clwwisshclwwslemlem  26926  erclwwlkstr  26936  erclwwlksntr  26948  clwlksfclwwlk  26962  frcond1  27130  frgr3v  27139  3vfriswmgr  27142  frgrwopreglem4a  27174  frrusgrord0lem  27203  numclwwlkffin  27214  numclwwlkovfel2  27216  extwwlkfab  27223  numclwlk1lem2f1  27227  numclwlk1lem2fo  27228  numclwwlk2lem1  27235  numclwlk2lem2f  27236  numclwlk2lem2f1o  27238  numclwwlk2  27240  frgrreggt1  27251  friendshipgt3  27256  imsmetlem  27545  nmoxr  27621  nmoolb  27626  blometi  27658  phpar2  27678  phpar  27679  ipasslem5  27690  hvadd32  27891  hvaddsub12  27895  hvaddsubass  27898  hvsubass  27901  hvsub32  27902  hvsubdistr1  27906  hvsubdistr2  27907  hvmulcan  27929  hvmulcan2  27930  hvsubcan  27931  his5  27943  his2sub  27949  hhssabloilem  28118  hhssnv  28121  shlej2  28220  pjoi0  28576  hodcl  28606  hoadd32  28642  hosubdi  28667  hosubsub2  28671  hoaddsubass  28674  hosubsub4  28677  nmoplb  28766  unop  28774  hmop  28781  nmfnlb  28783  lnopmul  28826  kbass1  28975  kbass2  28976  leopmul2i  28994  leoptr  28996  cvntr  29151  mdslmd4i  29192  mdexchi  29194  atcv1  29239  sumdmdii  29274  fcoinvbr  29419  fpwrelmapffs  29509  xreceu  29630  isinftm  29735  unitdivcld  29947  esummulc1  30143  hasheuni  30147  unelsiga  30197  inelpisys  30217  carsgsigalem  30377  signswmnd  30634  bnj545  30965  bnj594  30982  bnj1311  31092  cvmsf1o  31254  cvmscld  31255  lediv2aALT  31571  subdivcomb2  31612  gcd32  31637  fununiq  31667  trpredpo  31735  poseq  31750  frr3g  31779  sltres  31815  sltletr  31881  sletr  31883  nocvxmin  31894  dfrdg4  32058  brcolinear  32166  colinearex  32167  nn0prpwlem  32317  clsun  32323  fnemeet1  32361  fnemeet2  32362  fnejoin1  32363  fnejoin2  32364  eltail  32369  rdgeqoa  33218  curf  33387  poimirlem28  33437  cnambfre  33458  ftc1anclem4  33488  cocanfo  33512  f1ocan1fv  33521  metf1o  33551  ismtybnd  33606  ghomco  33690  isdrngo2  33757  inidl  33829  igenmin  33863  cmtvalN  34498  cvrval  34556  pmapmeet  35059  paddval  35084  paddssat  35100  elpcliN  35179  pclssN  35180  pclunN  35184  paddunN  35213  poldmj1N  35214  tendoplcl2  36066  tendoplcl  36069  dihmeet  36632  mapco2g  37277  mzpcompact2lem  37314  eqrabdioph  37341  lerabdioph  37369  eluzrabdioph  37370  ltrabdioph  37372  nerabdioph  37373  dvdsrabdioph  37374  reglogcl  37454  rmxyadd  37486  rmyabs  37525  congadd  37533  congabseq  37541  rmydioph  37581  mendring  37762  mendlmod  37763  iocinico  37797  relexp0a  38008  relexpaddss  38010  brcoffn  38328  dvconstbi  38533  uzwo4  39221  ssin0  39223  ssinc  39264  ssdec  39265  unima  39346  fvmpt2bd  39350  disjf1o  39378  ssnnf1octb  39382  sub31  39503  fperiodmullem  39517  ssfiunibd  39523  infxr  39583  fmul01  39812  islptre  39851  lptre2pt  39872  limcleqr  39876  limclner  39883  limsuppnflem  39942  limsupvaluz2  39970  supcnvlimsup  39972  xlimmnfvlem2  40059  xlimmnfv  40060  xlimpnfvlem2  40063  xlimpnfv  40064  climxlim2lem  40071  coskpi2  40077  cosknegpi  40080  dvnmptdivc  40153  dvdsn1add  40154  dvnmptconst  40156  dvmptfprod  40160  dvnprodlem1  40161  dvnprodlem2  40162  ovolsplit  40205  stoweidlem60  40277  stowei  40281  dirkeritg  40319  fourierdlem70  40393  fourierdlem71  40394  fourierdlem103  40426  fourierdlem104  40427  fouriersw  40448  rrxtopnfi  40506  saluncl  40537  salexct  40552  sge0ltfirp  40617  sge0iunmpt  40635  meadjiunlem  40682  carageniuncllem1  40735  caratheodorylem1  40740  ovncvrrp  40778  ovnsubaddlem1  40784  hspmbllem2  40841  ovolval5lem3  40868  smfpimbor1lem1  41005  smfsuplem1  41017  smflimsuplem4  41029  sigarls  41046  cnambpcma  41309  elfzelfzlble  41331  fzoopth  41337  m1mod0mod1  41339  fsumsplitsndif  41343  iccpartiltu  41358  pfxsuff1eqwrdeq  41407  ccatpfx  41409  pfx2  41412  pfxccatin12lem1  41423  fmtno4prmfac  41484  2pwp1prmfmtno  41504  lighneallem4b  41526  oexpnegALTV  41588  mogoldbblem  41629  gbegt5  41649  sbgoldbm  41672  nnsum3primesle9  41682  nnsum4primesodd  41684  nnsum4primesoddALTV  41685  evengpoap3  41687  nnsum4primesevenALTV  41689  isupwlk  41717  lidldomnnring  41930  2zrngacmnd  41942  rhmsubclem2  42087  rhmsubcALTVlem2  42105  xpprsng  42110  zlmodzxzscm  42135  gsumlsscl  42164  lincvalsng  42205  lincvalpr  42207  lincdifsn  42213  linc1  42214  lincellss  42215  difmodm1lt  42317  fdivmpt  42334  digexp  42401  amgmwlem  42548