Theorem 3adant2 1128

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

Hypothesis

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

Assertion

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

Proof of Theorem 3adant2

Step	Hyp	Ref	Expression
1		3adant.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	adantlr 713	. 2 ⊢ (((𝜑 ∧ 𝜃) ∧ 𝜓) → 𝜒)
3	2	3impa 1107	1 ⊢ ((𝜑 ∧ 𝜃 ∧ 𝜓) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1084

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 395  df-3an 1086

This theorem is referenced by:  3ad2ant1  1130  3simpb  1146  3imp3i2an  1342  eupickb  2624  vtoclegftOLD  3570  eqeu  3699  onunel  6473  iotan0  6536  funopg  6585  fncoOLD  6671  dff1o2  6840  fvelimad  6962  unima  6969  fnimapr  6978  fvmptt  7021  fnreseql  7053  xpprsng  7146  f1elima  7270  f13dfv  7280  f1ocnvfvb  7285  f1cdmsn  7288  f1ofvswap  7311  oprssov  7587  funelss  8053  poxp  8134  poxp2  8149  poxp3  8156  wfrlem4OLD  8334  smoiso  8384  oaord  8569  oaword  8571  omcan  8591  omwordri  8594  odi  8601  omeulem1  8604  oeord  8610  oecan  8611  oewordri  8614  oeordsuc  8616  nnaord  8641  nnaordr  8642  nndi  8645  nnaword  8649  nnmwordri  8658  naddel2  8710  naddss1  8711  naddss2  8712  erov  8835  ecopovtrn  8841  mapsnd  8907  f1dom3g  8990  xpdom3  9100  mapxpen  9173  dif1en  9190  dif1enOLD  9192  findcard  9193  f1domfi2  9212  entrfir  9221  domtrfil  9222  domtrfir  9224  sbthfilem  9228  sdomdomtrfi  9231  php3  9239  findcard3  9312  indexfi  9397  suppr  9507  infpr  9539  r111  9811  tcrank  9920  acndom  10087  infdif2  10244  infxpdom  10245  cfeq0  10290  cfsuc  10291  cfflb  10293  cflim2  10297  cfsmolem  10304  axcc3  10472  domtriomlem  10476  axdc3lem2  10485  axdc3lem4  10487  axdc4lem  10489  axcclem  10491  pwcfsdom  10617  tsktrss  10795  tsksuc  10796  tskuni  10817  adderpqlem  10988  mulerpqlem  10989  mulcanenq  10994  distrnq  10995  ltsonq  11003  ltanq  11005  ltmnq  11006  distrlem1pr  11059  distrlem5pr  11061  ltsopr  11066  ltsosr  11128  ltasr  11134  adddir  11246  axlttrn  11327  letr  11349  nnncan1  11537  npncan3  11539  pnpcan2  11541  subdi  11688  subdir  11689  mulcan1g  11908  mulcan2g  11909  divmul  11917  div23  11933  div13  11935  muldivdir  11952  divsubdir  11953  subdivcomb1  11954  divcan7  11968  ltmul2  12110  lemul1  12111  lemul2  12112  lemul2a  12114  lediv1  12125  ltmuldiv2  12134  lemuldiv  12140  lemuldiv2  12141  ltdiv2  12146  lediv2  12150  infrelb  12245  nndivtr  12305  bndndx  12517  nn0n0n1ge2  12585  fnn0ind  12707  addlelt  13136  xrletr  13185  qsqueeze  13228  xleadd2a  13281  xleadd1  13282  xltadd2  13284  xltmul2  13320  supxrbnd  13355  iooneg  13496  iccneg  13497  icoshft  13498  icoshftf1o  13499  zltaddlt1le  13530  fzen  13566  uzsubsubfz  13571  ssfzunsnext  13594  fzrevral2  13635  fzshftral  13637  fz0fzdiffz0  13658  elfzmlbp  13660  elfzo  13682  nelfzo  13685  fzoaddel2  13736  fzosubel2  13740  ssfzo12bi  13775  fzonfzoufzol  13784  subfzo0  13803  flltdivnn0lt  13847  modmulnn  13903  modcyc  13920  modaddabs  13923  modaddmod  13924  modmuladd  13927  modadd2mod  13935  modsubmod  13943  modsubmodmod  13944  modaddmodup  13948  modmulmod  13950  modsubdir  13954  modfzo0difsn  13957  modsumfzodifsn  13958  uzindi  13996  axdc4uzlem  13997  expneg2  14084  expdiv  14127  expubnd  14190  mulbinom2  14235  bernneq2  14242  expnngt1  14253  hashinfxadd  14397  hashunsngx  14405  hashunsnggt  14406  hashfundm  14454  hashf1dmcdm  14456  hashdifsnp1  14510  ccatval3  14582  ccatfv0  14586  ccatval1lsw  14587  ccats1val2  14630  ccatw2s1p1  14639  swrdnd  14657  pfxsuffeqwrdeq  14701  pfxsuff1eqwrdeq  14702  swrdswrd  14708  pfxpfx  14711  wrd2ind  14726  swrdccatin1  14728  pfxccatin12lem1  14731  swrdccatin2  14732  pfxccatin12lem3  14735  swrdccat  14738  pfxccatpfx1  14739  pfxccatpfx2  14740  swrdccat3blem  14742  repswswrd  14787  repswpfx  14788  repswccat  14789  cshwidxmod  14806  2cshw  14816  3cshw  14821  scshwfzeqfzo  14830  cshwcsh2id  14832  cshimadifsn  14833  cshimadifsn0  14834  ccatco  14839  cshco  14840  swrdco  14841  pfxco  14842  lswco  14843  swrds2  14944  2swrd2eqwrdeq  14957  shftuz  15069  abs3dif  15331  fsumdifsnconst  15790  modfsummods  15792  sin02gt0  16189  dvdsval2  16254  dvdscmul  16280  dvdsmulc  16281  dvdscmulr  16282  dvdsmulcr  16283  divalglem8  16397  ndvdssub  16406  dvdsexpim  16551  rpmulgcd  16553  expgcd  16559  zexpgcd  16561  coprmprod  16657  cncongr1  16663  cncongr2  16664  isprm3  16679  modprm0  16802  coprimeprodsq  16805  pythagtriplem12  16823  pythagtriplem14  16825  pcprendvds  16837  pcmul  16848  pcdiv  16849  pcqcl  16853  pcqdiv  16854  pcdvdsb  16866  vdwnnlem1  16992  hashbcss  17001  cshwshashlem1  17093  fvsetsid  17165  setsstruct2  17171  setsstruct  17173  mrcss  17624  mrcsscl  17628  mrcun  17630  cofulid  17904  catcisolem  18127  funcsetcestrclem9  18182  latleeqj1  18471  lubun  18535  clatleglb  18538  pslem  18592  dirtr  18622  mgmb1mgm1  18643  pwspjmhm  18815  grpinvid1  18981  grpinvid2  18982  grpasscan1  18991  grpasscan2  18992  grpinvadd  19008  grpsubf  19009  grpsubrcan  19011  grpinvsub  19012  grpsubeq0  19016  grpsubadd0sub  19017  grppncan  19021  grpnpcan  19022  mulgnn0p1  19075  mulgaddcomlem  19087  mulginvcom  19089  mulginvinv  19090  subgsubcl  19127  subgsub  19128  eqglact  19169  qussub  19181  ghmsub  19214  psgnunilem4  19491  oddvds2  19560  odsubdvds  19565  gexnnod  19582  slwn0  19609  dvrcl  20382  unitdvcl  20383  dvrcan1  20387  dvrcan3  20388  dvreq1  20389  rngisom1  20444  rngisomring  20445  subrgdv  20569  abvsubtri  20802  idsrngd  20831  lmodvsubval2  20889  lsmcl  21057  lsmsp2  21061  lspsntrim  21072  rngqiprngimfolem  21275  lidldvgen  21319  cncrng  21376  chrcong  21517  dvdschrmulg  21518  zndvds  21543  zntoslem  21550  ocvsscon  21667  obselocv  21722  frlmphl  21775  ascldimul  21881  mpfsubrg  22114  ply1tmcl  22259  eqcoe1ply1eq  22287  gsummoncoe1  22296  lply1binomsc  22299  mamudm  22383  mamufacex  22384  scmatf1  22521  scmatf1o  22522  scmatrngiso  22526  submabas  22568  mdetdiaglem  22588  mdetralt2  22599  mdetero  22600  mdetunilem2  22603  mdetunilem6  22607  m2detleiblem7  22617  maducoeval2  22630  gsummatr01lem3  22647  gsummatr01  22649  smadiadetglem2  22662  cramerlem1  22677  mply1topmatcl  22795  mp2pm2mplem4  22799  ntrin  23053  elnei  23103  neindisj2  23115  ordtopn3  23188  leordtval2  23204  lecldbas  23211  cnrest2  23278  cmpsublem  23391  ptrescn  23631  xkococn  23652  kqfeq  23716  snfbas  23858  neifil  23872  fclsrest  24016  utopsnnei  24242  neipcfilu  24289  psmetsym  24304  psmetge0  24306  xmetge0  24338  xmetsym  24341  metustto  24550  metustbl  24563  restmetu  24567  nm2dif  24622  nmtri  24623  cnmet  24776  cnmpopc  24937  iihalf1  24940  iihalf2  24943  iocopnst  24952  clmnegsubdi2  25120  clmsub4  25121  clmvsubval2  25125  ncvspi  25172  cphsqrtcl3  25203  cph2ass  25229  cphipval2  25257  cphipval  25259  caublcls  25325  bcthlem3  25342  bcthlem4  25343  srabn  25376  cssbn  25391  cmslsschl  25393  rrxmet  25424  rrxdsfi  25427  iblconst  25835  tdeglem3OLD  26082  dvdsq1p  26187  coeid3  26264  aannenlem2  26354  pserdvlem2  26455  tanord1  26561  cxpef  26689  recxpcl  26699  logbchbase  26796  relogbcl  26798  relogbzcl  26799  logbleb  26808  logblt  26809  relogbcxpb  26812  lawcos  26841  pythag  26842  isosctrlem1  26843  isosctrlem2  26844  lgsmodeq  27368  lgsmulsqcoprm  27369  gausslemma2dlem1a  27391  2lgsoddprmlem2  27435  sltres  27689  sletr  27785  cofcutr  27938  lrrecpo  27952  sltadd2im  27997  sleadd2im  27999  sleadd1  28000  sleadd2  28001  sltadd1  28003  addscan2  28004  addscan1  28005  sltsub1  28080  divsmulw  28190  ax5seglem1  28859  axcontlem2  28896  axcontlem8  28902  upgrpredgv  29072  numedglnl  29077  issubgr2  29205  uhgrissubgr  29208  egrsubgr  29210  nbusgrfi  29307  nb3grprlem2  29314  cplgr3v  29368  cusgrsizeindslem  29385  finsumvtxdg2size  29484  rusgrpropadjvtx  29519  upgrwlkvtxedg  29579  usgr2trlncl  29694  uspgrn2crct  29739  crctcshwlkn0lem4  29744  crctcshwlkn0lem5  29745  wwlksnextproplem3  29842  umgr2adedgwlklem  29875  rusgr0edg  29904  clwwlk1loop  29918  clwwlkccatlem  29919  clwlkclwwlklem2a4  29927  clwlkclwwlklem2a  29928  clwwisshclwwslemlem  29943  erclwwlktr  29952  clwwlkel  29976  erclwwlkntr  30001  clwwlknonex2lem2  30038  uhgr3cyclex  30112  umgr3cyclex  30113  eucrctshift  30173  frgr3v  30205  3cyclfrgrrn  30216  frgrwopreglem5a  30241  frgr2wsp1  30260  extwwlkfab  30282  clwwlknonclwlknonf1o  30292  numclwwlk3lem1  30312  numclwwlk5  30318  numclwwlk6  30320  isgrpo  30427  grpoinvid1  30458  grpoinvid2  30459  grpoinvop  30463  grpodivinv  30466  grpoinvdiv  30467  grpodivf  30468  grponpcan  30473  ablonncan  30486  nvmval  30572  nvmval2  30573  nvmfval  30574  nvmul0or  30580  nvpncan2  30583  nvaddsub4  30587  nvmeq0  30588  nvdif  30596  nvpi  30597  nvmtri  30601  nvabs  30602  imsmetlem  30620  ipval2lem3  30635  ipval2  30637  4ipval2  30638  ipval3  30639  nmooge0  30697  blometi  30733  hvaddsub12  30968  hvsubdistr1  30979  hvsubdistr2  30980  hvaddcan2  31001  hvmulcan  31002  hvmulcan2  31003  hvsubcan  31004  hvsubcan2  31005  his7  31020  his2sub  31022  his2sub2  31023  norm3dif2  31081  shsubcl  31150  hhssnv  31194  shlej2  31291  fh2  31549  cm2j  31550  pjoi0  31647  hodcl  31677  hosubdi  31738  unopf1o  31846  unopadj  31849  adj2  31864  braadd  31875  bramul  31876  lnopaddmuli  31903  lnopsubmuli  31905  homco2  31907  lnfnaddmuli  31975  adjlnop  32016  leopmul  32064  leoptr  32067  pjimai  32106  atcv1  32310  atexch  32311  atcvatlem  32315  fcoinvbr  32525  preiman0  32621  divnumden2  32719  xdivmul  32789  cshf1o  32829  resvsca  33209  idlsrgcmnd  33396  hasheuni  33931  difelsiga  33979  cndprobin  34281  bayesth  34286  sgn3da  34388  signstfvp  34430  breprexplemc  34491  fineqvac  34946  swrdrevpfx  34957  swrdwlk  34967  lediv2aALT  35518  fununiq  35605  dfrdg2  35632  clsun  36053  neiin  36057  rdgeqoa  37090  curfv  37314  matunitlindflem1  37330  poimirlem32  37366  ftc1anclem4  37410  areacirc  37427  filbcmb  37454  ismtybnd  37521  grpoeqdivid  37595  ghomco  37605  rngonegrmul  37658  zerdivemp1x  37661  rngohomco  37688  rngoisoco  37696  riscer  37702  intidl  37743  isfldidl  37782  brredunds  38337  lshpnelb  38695  opnlen0  38899  opcon3b  38907  opcon2b  38908  oplecon3b  38911  opltcon3b  38915  opltcon2b  38917  oldmm1  38928  oldmm4  38931  oldmj1  38932  oldmj4  38935  cvrval2  38985  cvrcon3b  38988  leatb  39003  atcmp  39022  atcvreq0  39025  atlatle  39031  athgt  39168  3dim2  39180  islln2a  39229  lplnnleat  39254  lvolnleat  39295  4atlem10  39318  4atlem11  39321  4atlem12  39324  dalem21  39406  dalem22  39407  dalem23  39408  dalem29  39413  dalem30  39414  dalem31N  39415  dalem32  39416  dalem33  39417  dalem34  39418  dalem35  39419  dalem36  39420  dalem37  39421  dalem40  39424  dalem46  39430  dalem47  39431  dalem51  39435  dalem52  39436  dalem58  39442  dalem59  39443  pmaple  39473  paddclN  39554  pmapjoin  39564  pmapjat1  39565  elpcliN  39605  pclssN  39606  pclun2N  39611  2polcon4bN  39630  paddunN  39639  poldmj1N  39640  pmapj2N  39641  pmapocjN  39642  psubclinN  39660  paddatclN  39661  poml4N  39665  lautco  39809  ldilco  39828  ltrneq2  39860  trljat1  39878  cdlemc1  39903  cdleme10  39966  ltrnco  40431  trlcocnv  40432  trljco  40452  trljco2  40453  cdlemi1  40530  tendocnv  40733  diaord  40759  dibord  40871  dihord3  40969  dihord4  40970  dihmeetlem2N  41011  dihmeetlem4preN  41018  dochdmj1  41102  hdmap10lem  41551  lcmineqlem1  41741  sticksstones2  41859  metakunt29  41941  metakunt30  41942  factwoffsmonot  41950  readdsub  42095  reltsub1  42097  renpncan3  42102  reppncan  42104  resubdi  42107  readdcan2  42123  mzprename  42443  dvdsrabdioph  42504  pell14qrdivcl  42559  monotoddzz  42638  jm2.19lem2  42685  jm2.19  42688  relexpaddss  43422  k0004lem3  43853  dvconstbi  44045  chordthmALT  44646  isosctrlem1ALT  44647  ssinc  44725  ssdec  44726  wessf1ornlem  44828  disjf1o  44834  ssnnf1octb  44837  projf1o  44840  mapssbi  44856  iunmapsn  44860  upbdrech  44956  iuneqfzuzlem  44985  suplesup  44990  rexabslelem  45069  climxrrelem  45406  limsupresxr  45423  liminfresxr  45424  liminfvalxr  45440  xlimliminflimsup  45519  cncfshift  45531  cncfperiod  45536  cncfuni  45543  icccncfext  45544  dvmptfprodlem  45601  dvnprodlem1  45603  itgspltprt  45636  ismbl3  45643  stoweidlem3  45660  stoweidlem10  45667  stoweidlem19  45676  stoweidlem31  45688  stoweidlem34  45691  stoweidlem44  45701  fourierdlem41  45805  fourierdlem42  45806  fourierdlem51  45814  fourierdlem68  45831  fourierdlem89  45852  fourierdlem91  45854  fourierdlem92  45855  fourierdlem94  45857  etransclem24  45915  etransclem34  45925  qndenserrnbllem  45951  salincl  45981  saldifcl2  45985  subsalsal  46016  sge0pr  46051  sge0pnffigt  46053  sge0reuz  46104  nnfoctbdjlem  46112  nnfoctbdj  46113  meadjiunlem  46122  caratheodorylem2  46184  hoidmv1le  46251  hoidmvlelem3  46254  hspmbllem2  46284  opnvonmbllem2  46290  sssmf  46395  smfaddlem1  46420  sigaraf  46510  sigarmf  46511  nltle2tri  46962  subsubelfzo0  46975  iccpartiltu  47030  icceuelpart  47044  poprelb  47132  reuopreuprim  47134  proththd  47222  mogoldbblem  47328  fppr2odd  47339  fpprel2  47349  bgoldbtbndlem2  47414  clnbusgrfi  47446  grimuhgr  47493  uhgrimisgrgric  47514  clnbgrgrim  47517  nn0sumltlt  47765  invginvrid  47782  ply1sclrmsm  47802  linccl  47833  lincvalpr  47837  lincresunit3lem1  47898  lincresunit3  47900  fdivmpt  47964  nnolog2flm1  48014  dignnld  48027  digexp  48031  dignn0flhalflem1  48039  itcovalsucov  48092  reorelicc  48134  eenglngeehlnmlem1  48161  line2  48176  line2xlem  48177  itsclc0lem1  48180  itsclc0xyqsolr  48193  i0oii  48289  io1ii  48290  indthinc  48409  indthincALT  48410  setrec2fun  48474  reccot  48540  rectan  48541