Theorem 3adant1 1072

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 1053	. 2 ⊢ ((𝜃 ∧ 𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜓))
2		3adant.1	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3	1, 2	syl 17	1 ⊢ ((𝜃 ∧ 𝜑 ∧ 𝜓) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  3ad2ant2  1076  3ad2ant3  1077  eupickb  2526  sbciegft  3433  reuhyp  4822  funopg  5836  funprg  5854  funtpg  5856  funcnvtp  5865  fvun1  6179  fnreseql  6235  ftpg  6328  f13dfv  6430  mpt2eq3ia  6618  ordunel  6919  fex2  7014  poxp  7176  suppval1  7188  wfr3g  7300  smores3  7337  oaord  7514  oacan  7515  oaword  7516  omord  7535  omcan  7536  omwordri  7539  odi  7546  omass  7547  oeord  7555  oecan  7556  oewordri  7559  oeordsuc  7561  nnaord  7586  nnaordr  7587  nndi  7590  nnmass  7591  nnaword  7594  nnmord  7599  nnmwordri  7603  erov  7731  ecopovtrn  7737  ixpf  7816  mapxpen  8011  fimax2g  8091  unbnn  8101  funisfsupp  8163  inelfi  8207  elfiun  8219  sup0  8255  suppr  8260  infpr  8292  r111  8521  dif1card  8716  xpcdaen  8888  mapcdaen  8889  ackbij1lem16  8940  cff1  8963  cfflb  8964  cfsmolem  8975  fin23lem34  9051  hsmexlem2  9132  axcc3  9143  domtriomlem  9147  axdc3lem4  9158  axdc4lem  9160  axcclem  9162  konigthlem  9269  gchdomtri  9330  tskpr  9471  tskop  9472  tskuni  9484  tskun  9487  gruop  9506  gruun  9507  grudomon  9518  adderpqlem  9655  mulerpqlem  9656  addassnq  9659  mulassnq  9660  distrnq  9662  ltsonq  9670  ltanq  9672  ltmnq  9673  genpass  9710  distrlem1pr  9726  distrlem4pr  9727  ltsopr  9733  adddir  9910  axlttrn  9989  ltletr  10008  letr  10010  mul32  10082  mul31  10083  add32  10133  subsub23  10165  addsubass  10170  subcan2  10185  subsub2  10188  nppcan2  10191  sub32  10194  nnncan  10195  nnncan2  10197  pnpcan2  10200  subdi  10342  subdir  10343  receu  10551  mulcan1g  10559  mulcan2g  10560  divmul3  10569  divrec  10580  divrec2  10581  divsubdir  10600  divdiv1  10615  redivcl  10623  div2neg  10627  ltmul2  10753  lemul1  10754  lemul2  10755  lemul2a  10757  lediv1  10767  gt0div  10768  ge0div  10769  mulsuble0b  10774  ltdivmul  10777  ledivmul  10778  ltdivmul2  10779  ledivmul2  10781  lemuldiv  10782  ltdiv23  10793  lediv23  10794  ledivp1i  10828  ltdivp1i  10829  uzind2  11346  nn0ind  11348  fnn0ind  11352  uz3m2nn  11607  xrltletr  11864  xrletr  11865  xrre2  11875  xrltmin  11887  xrlemin  11889  xleadd2a  11956  xleadd1  11957  xltadd2  11959  xmulasslem3  11988  xmulass  11989  xltmul2  11995  ixxdisj  12061  iooneg  12163  iccneg  12164  icoshft  12165  icoshftf1o  12166  icodisj  12168  snunioo  12169  fzen  12229  ssfzunsn  12257  fzrev3  12276  2ffzeq  12329  fzoaddel2  12391  elfzodifsumelfzo  12401  ssfzoulel  12428  ssfzo12bi  12429  fzoshftral  12447  adddivflid  12481  flltdivnn0lt  12496  ltdifltdiv  12497  fldiv4p1lem1div2  12498  modcyc  12567  modcyc2  12568  modaddabs  12570  modsubmodmod  12591  modaddmodup  12595  modaddmulmod  12599  moddi  12600  modsubdir  12601  expdiv  12773  digit2  12859  hashdifpr  13064  fi1uzind  13134  fi1uzindOLD  13140  ccatass  13224  lswccatn0lsw  13226  swrdval  13269  swrdnd  13284  swrd0  13286  swrdfv2  13298  2swrd1eqwrdeq  13306  swrdswrdlem  13311  swrdccatin12lem2a  13336  swrdccatin12lem2b  13337  repswccat  13383  cshwidxmod  13400  cshwidxmodr  13401  cshf1  13407  repswcshw  13409  2cshw  13410  2cshwcom  13413  2cshwcshw  13422  cshwcsh2id  13425  ccatco  13432  2swrd2eqwrdeq  13544  wwlktovf  13547  brcnvtrclfv  13592  shftval2  13663  mulre  13709  absdiv  13883  absdiflt  13905  absdifle  13906  abs3dif  13919  cau3  13943  ello12r  14096  elo12r  14107  modfsummods  14366  geoisum1c  14450  rpnnen2lem4  14785  rpnnen2lem7  14788  dvdsmulc  14847  dvdsmulcr  14849  dvdsmultr1  14857  dvdsmultr2  14859  dvdssub2  14861  oexpneg  14907  divalgb  14965  ndvdsadd  14972  sadass  15031  modgcd  15091  dvdsgcd  15099  dvdsgcdb  15100  gcdass  15102  mulgcd  15103  absmulgcd  15104  rpmulgcd  15113  nn0seqcvgd  15121  algcvga  15130  lcmdvdsb  15164  lcmass  15165  lcmfunsnlem1  15188  lcmfunsnlem2lem1  15189  lcmfunsnlem2lem2  15190  coprmdvds  15204  coprmdvdsOLD  15205  coprmdvds2  15206  rpmul  15211  cncongr1  15219  cncongr2  15220  prmgt1  15247  qnumdenbi  15290  modprm0  15348  coprimeprodsq  15351  pythagtriplem4  15362  pythagtriplem8  15366  pythagtriplem9  15367  pythagtriplem12  15369  pythagtriplem14  15371  pythagtriplem16  15373  pcpremul  15386  pcgcd  15420  vdwapval  15515  vdwapun  15516  prmgaplem3  15595  prmgaplem4  15596  prmgaplem7  15599  prmgapprmolem  15603  setsstruct  15727  mreiincl  16079  mreincl  16082  mremre  16087  mrcss  16099  catcisolem  16579  pleval2  16788  pospo  16796  latlem  16872  latjcom  16882  latmcom  16898  lubss  16944  lubun  16946  clatglbss  16950  ipole  16981  ipolt  16982  pslem  17029  dirtr  17059  gsumws2  17202  frmdmnd  17219  isgrpi  17268  grpsubrcan  17319  grpinvsub  17320  grpsubeq0  17324  grpsubadd0sub  17325  grpnpcan  17330  qussub  17477  ghmsub  17491  symggrp  17643  symgextsymg  17667  gsmsymgreqlem2  17674  symgfixfolem1  17681  pmtrprfv3  17697  symggen  17713  lsmass  17906  efgsrel  17970  cntzcmn  18068  dvrcl  18509  unitdvcl  18510  dvrcan1  18514  subrgmre  18627  abvsubtri  18658  abvtrivd  18663  lmodvsubval2  18741  lss0cl  18768  lssintcl  18785  lssincl  18786  reslmhm2  18874  lspvadd  18917  lspsntrim  18919  islbs3  18976  rrgeq0  19111  evlsval2  19341  cncrng  19586  xrsmcmn  19588  cndrng  19594  cnsrng  19599  xrs1mnd  19603  absabv  19622  psgnco  19748  zrhpsgninv  19750  zrhpsgnevpm  19756  zrhpsgnodpm  19757  zrhpsgnelbas  19759  zrhcopsgnelbas  19760  uvcresum  19951  lindfmm  19985  lindsmm  19986  mamudm  20013  mamufacex  20014  matsubgcell  20059  matsc  20075  scmatscmide  20132  scmatrhmcl  20153  1marepvsma1  20208  m1detdiag  20222  mdetralt  20233  m2detleiblem7  20252  gsummatr01lem3  20282  gsummatr01  20284  smadiadetlem0  20286  decpmate  20390  decpmatcl  20391  pm2mpcl  20421  pm2mpghmlem2  20436  chfacfscmul0  20482  chfacfscmulgsum  20484  chfacfpmmul0  20486  chfacfpmmulgsum  20488  unopn  20533  clsss  20668  cldmre  20692  toponmre  20707  opnssneib  20729  restabs  20779  restcls  20795  restntr  20796  hausnei2  20967  cmpsublem  21012  bwth  21023  hausmapdom  21113  ptpjcn  21224  upxp  21236  ptrescn  21252  xkopjcn  21269  fbssfi  21451  snfil  21478  ufprim  21523  rnelfm  21567  flimrest  21597  fclsrest  21638  tmdgsum  21709  blpnfctr  22051  mscl  22076  xmscl  22077  xmsge0  22078  xmseq0  22079  restmetu  22185  ngpds  22218  tngngp3  22270  unitnmn0  22282  xrsxmet  22420  metds0  22461  cncfmptc  22522  isclmp  22705  cnlmod  22748  ncvsi  22759  cphsqrtcl  22792  cfil3i  22875  cfilres  22902  cmmbl  23109  voliunlem2  23126  itg2ub  23306  itgrecl  23370  tdeglem3  23623  r1pid  23723  eflogeq  24152  cxpadd  24225  logbchbase  24309  relogbreexp  24313  relogbzexp  24314  relogbmulexp  24316  logbleb  24321  logblt  24322  lawcos  24346  pythag  24347  asinsinb  24424  acoscosb  24425  atantanb  24451  amgmlem  24516  lgsneg  24846  lgsne0  24860  lgsmodeq  24867  lgsmulsqcoprm  24868  gausslemma2dlem1a  24890  brbtwn2  25585  colinearalg  25590  eleesubd  25592  axcgrrflx  25594  axcgrtr  25595  axsegcon  25607  ax5seglem1  25608  ax5seglem2  25609  ax5seglem4  25612  axbtwnid  25619  axlowdimlem14  25635  axlowdim  25641  axcontlem5  25648  axcontlem7  25650  funvtxdmge2val  25691  funiedgdmge2val  25692  nb3graprlem2  25981  cusgra3v  25993  cusgrasizeindslem2  26003  sizeusglecusglem2  26013  iswlkg  26052  edgwlk  26059  usgrwlknloop  26093  spthonepeq  26117  constr2spth  26130  constr2pth  26131  redwlk  26136  usgra2adedgwlkonALT  26144  cyclispthon  26161  usgrcyclnl1  26168  usgrcyclnl2  26169  3v3e3cycl1  26172  constr3lem5  26176  constr3trllem2  26179  constr3pthlem2  26184  4cycl4v4e  26194  4cycl4dv4e  26196  wwlknimp  26215  wlkiswwlk1  26218  wlkiswwlk2lem4  26222  wlkiswwlk2lem6  26224  usg2wlkeq  26236  usg2wlkeq2  26237  wlkiswwlkinj  26246  wlkiswwlksur  26247  wwlknred  26251  wwlknextbi  26253  isclwlkg  26283  clwlkisclwwlklem2a1  26307  clwlkisclwwlklem2a4  26312  clwlkisclwwlklem2a  26313  clwlkisclwwlk  26317  clwlkisclwwlk2  26318  clwwlkf  26322  wwlksubclwwlk  26332  clwwisshclwwlem1  26333  erclwwlktr  26343  eleclclwwlknlem1  26345  usg2cwwkdifex  26349  erclwwlkntr  26355  hashecclwwlkn1  26361  usghashecclwwlk  26362  hashclwwlkn  26363  clwlkfclwwlk  26371  el2spthonot  26397  el2spthonot0  26398  usg2wlkonot  26410  vdgrfval  26422  rusgrargra  26457  rusgranumwlklem4  26479  frgra3v  26529  3vfriswmgra  26532  frgrawopreg  26576  frg2woteu  26582  frgregordn0  26597  extwwlkfablem2lem  26602  numclwwlkovfel2  26610  numclwwlkovf2ex  26613  numclwwlkovgelim  26616  extwwlkfab  26617  numclwlk1lem2f1  26621  numclwlk1lem2fo  26622  numclwwlk2lem1  26629  numclwlk2lem2f  26630  numclwlk2lem2f1o  26632  frgrareggt1  26643  frgrareg  26644  frgraregord013  26645  friendshipgt3  26648  imsmetlem  26929  nmoxr  27005  nmoolb  27010  blometi  27042  phpar2  27062  phpar  27063  ipasslem5  27074  hvadd32  27275  hvaddsub12  27279  hvaddsubass  27282  hvsubass  27285  hvsub32  27286  hvsubdistr1  27290  hvsubdistr2  27291  hvmulcan  27313  hvmulcan2  27314  hvsubcan  27315  his5  27327  his2sub  27333  hhssabloilem  27502  hhssnv  27505  shlej2  27604  pjoi0  27960  hodcl  27990  hoadd32  28026  hosubdi  28051  hosubsub2  28055  hoaddsubass  28058  hosubsub4  28061  nmoplb  28150  unop  28158  hmop  28165  nmfnlb  28167  lnopmul  28210  kbass1  28359  kbass2  28360  leopmul2i  28378  leoptr  28380  cvntr  28535  mdslmd4i  28576  mdexchi  28578  atcv1  28623  sumdmdii  28658  fcoinvbr  28799  fpwrelmapffs  28897  xreceu  28961  isinftm  29066  unitdivcld  29275  esummulc1  29470  hasheuni  29474  unelsiga  29524  inelpisys  29544  carsgsigalem  29704  signswmnd  29960  bnj545  30219  bnj594  30236  bnj1311  30346  cvmsf1o  30508  cvmscld  30509  lediv2aALT  30825  subdivcomb2  30865  gcd32  30890  fununiq  30913  trpredpo  30979  poseq  30994  frr3g  31023  sltres  31061  nocvxmin  31090  dfrdg4  31228  brcolinear  31336  colinearex  31337  nn0prpwlem  31487  clsun  31493  fnemeet1  31531  fnemeet2  31532  fnejoin1  31533  fnejoin2  31534  eltail  31539  rdgeqoa  32394  curf  32557  poimirlem28  32607  cnambfre  32628  ftc1anclem4  32658  cocanfo  32682  f1ocan1fv  32691  metf1o  32721  ismtybnd  32776  ghomco  32860  isdrngo2  32927  inidl  32999  igenmin  33033  cmtvalN  33516  cvrval  33574  pmapmeet  34077  paddval  34102  paddssat  34118  elpcliN  34197  pclssN  34198  pclunN  34202  paddunN  34231  poldmj1N  34232  tendoplcl2  35084  tendoplcl  35087  dihmeet  35650  mapco2g  36295  mzpcompact2lem  36332  eqrabdioph  36359  lerabdioph  36387  eluzrabdioph  36388  ltrabdioph  36390  nerabdioph  36391  dvdsrabdioph  36392  reglogcl  36472  rmxyadd  36504  rmyabs  36543  congadd  36551  congabseq  36559  rmydioph  36599  mendring  36781  mendlmod  36782  iocinico  36816  relexp0a  37027  relexpaddss  37029  brcoffn  37348  dvconstbi  37555  uzwo4  38246  ssinc  38292  ssdec  38293  unima  38340  fvmpt2bd  38345  disjf1o  38373  ssnnf1octb  38377  sub31  38444  fperiodmullem  38458  ssfiunibd  38464  infxr  38524  fmul01  38647  islptre  38686  lptre2pt  38707  limcleqr  38711  limclner  38718  coskpi2  38749  cosknegpi  38752  dvnmptdivc  38828  dvdsn1add  38829  dvnmptconst  38831  dvmptfprod  38835  dvnprodlem1  38836  dvnprodlem2  38837  ovolsplit  38881  stoweidlem60  38953  stowei  38957  dirkeritg  38995  fourierdlem70  39069  fourierdlem71  39070  fourierdlem103  39102  fourierdlem104  39103  fouriersw  39124  rrxtopnfi  39182  saluncl  39213  salexct  39228  sge0ltfirp  39293  sge0iunmpt  39311  meadjiunlem  39358  carageniuncllem1  39411  caratheodorylem1  39416  ovncvrrp  39454  ovnsubaddlem1  39460  hspmbllem2  39517  ovolval5lem3  39544  smfpimbor1lem1  39683  sigarls  39695  m1mod0mod1  39949  iccpartiltu  39960  fmtno4prmfac  40022  2pwp1prmfmtno  40042  lighneallem4b  40064  oexpnegALTV  40126  gbegt5  40183  nnsum3primesle9  40210  nnsum4primesodd  40212  nnsum4primesoddALTV  40213  evengpoap3  40215  nnsum4primesevenALTV  40217  pfxsuff1eqwrdeq  40270  ccatpfx  40272  pfx2  40275  pfxccatin12lem1  40286  cnambpcma  40341  elfzelfzlble  40358  fzoopth  40360  nfile  40369  fsumsplitsndif  40372  uhgruhgra  40375  uhgrauhgrbi  40377  usgr1v0e  40545  nb3grprlem2  40609  cplgr3v  40657  cusgrsizeindslem  40667  sizusglecusglem2  40678  umgr2v2e  40741  cusgrrusgr  40781  is1wlk  40813  isWlk  40814  uspgr2wlkeq  40854  uspgr2wlkeq2  40855  uspgr2wlkeqi  40856  wlkOn2n0  40874  pthdadjvtx  40936  upgr2pthnlp  40938  spthonepeq-av  40958  usgr2wlkspth  40965  pthdlem2lem  40973  uspgrn2crct  41011  crctcsh1wlkn0lem3  41015  crctcsh1wlkn0lem5  41017  1wlkiswwlks2lem4  41069  1wlkiswwlks2lem6  41071  1wlklnwwlkln2lem  41079  wwlksnred  41098  wwlksnextbi  41100  wwlksnextwrd  41103  2pthdlem1  41137  21wlkdlem10  41142  umgr2adedgwlkonALT  41154  elwwlks2ons3  41159  s3wwlks2on  41160  elwspths2on  41163  clwwlknp  41195  isclwwlksng  41196  clwlkclwwlklem2a4  41206  clwlkclwwlklem2a  41207  clwlkclwwlk  41211  clwlkclwwlk2  41212  clwwlksgt0  41213  clwwlksf  41222  wwlksubclwwlks  41232  clwwisshclwwslemlem  41233  erclwwlkstr  41243  erclwwlksntr  41255  clwlksfclwwlk  41269  upgreupthi  41376  frcond1  41438  frgr3v  41445  3vfriswmgr  41448  frgrwopreg  41486  frgr2wwlkeu  41492  frrusgrord0  41503  av-extwwlkfablem2lem  41507  av-numclwwlkffin  41512  av-numclwwlkovfel2  41514  av-numclwwlkovf2ex  41517  av-extwwlkfab  41520  av-numclwlk1lem2f1  41524  av-numclwlk1lem2fo  41525  av-numclwwlk2lem1  41532  av-numclwlk2lem2f  41533  av-numclwlk2lem2f1o  41535  av-numclwwlk2  41537  av-frgrareggt1  41547  av-friendshipgt3  41552  lidldomnnring  41720  2zrngacmnd  41732  rhmsubclem2  41879  rhmsubcALTVlem2  41898  xpprsng  41903  zlmodzxzscm  41928  gsumlsscl  41958  lincvalsng  41999  lincvalpr  42001  lincdifsn  42007  linc1  42008  lincellss  42009  difmodm1lt  42111  fdivmpt  42132  digexp  42199  amgmwlem  42357