Theorem 3adant2 1124

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1080

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 208  df-an 397  df-3an 1082

This theorem is referenced by:  3ad2ant1  1126  3simpb  1142  3imp3i2an  1338  eupickb  2689  vtoclegft  3523  eqeu  3634  funopg  6262  fnco  6338  dff1o2  6491  fvelimad  6603  fnimapr  6617  fvmptt  6657  fnreseql  6686  xpprsng  6768  f1elima  6889  f13dfv  6899  f1ocnvfvb  6904  oprssov  7176  funelss  7605  poxp  7678  wfrlem4  7812  wfrlem4OLD  7813  smoiso  7854  oaord  8026  oaword  8028  omcan  8048  omwordri  8051  odi  8058  omeulem1  8061  oeord  8067  oecan  8068  oewordri  8071  oeordsuc  8073  nnaord  8098  nnaordr  8099  nndi  8102  nnaword  8106  nnmwordri  8115  erov  8247  ecopovtrn  8253  mapsnd  8302  xpdom3  8465  mapxpen  8533  findcard  8606  indexfi  8681  suppr  8784  infpr  8816  r111  9053  tcrank  9162  acndom  9326  infdif2  9481  infxpdom  9482  cfeq0  9527  cfsuc  9528  cfflb  9530  cflim2  9534  cfsmolem  9541  axcc3  9709  domtriomlem  9713  axdc3lem2  9722  axdc3lem4  9724  axdc4lem  9726  axcclem  9728  pwcfsdom  9854  tsktrss  10032  tsksuc  10033  tskuni  10054  adderpqlem  10225  mulerpqlem  10226  mulcanenq  10231  distrnq  10232  ltsonq  10240  ltanq  10242  ltmnq  10243  distrlem1pr  10296  distrlem5pr  10298  ltsopr  10303  ltsosr  10365  ltasr  10371  adddir  10481  axlttrn  10562  letr  10583  nnncan1  10772  npncan3  10774  pnpcan2  10776  subdi  10923  subdir  10924  mulcan1g  11143  mulcan2g  11144  divmul  11151  div23  11167  div13  11169  muldivdir  11183  divsubdir  11184  subdivcomb1  11185  divcan7  11199  ltmul2  11341  lemul1  11342  lemul2  11343  lemul2a  11345  lediv1  11355  ltmuldiv2  11364  lemuldiv  11370  lemuldiv2  11371  ltdiv2  11376  lediv2  11380  fiminreOLD  11440  infrelb  11476  nndivtr  11534  bndndx  11746  nn0n0n1ge2  11812  fnn0ind  11931  addlelt  12353  xrletr  12401  qsqueeze  12444  xleadd2a  12497  xleadd1  12498  xltadd2  12500  xltmul2  12536  supxrbnd  12571  iooneg  12707  iccneg  12708  icoshft  12709  icoshftf1o  12710  zltaddlt1le  12740  fzen  12774  uzsubsubfz  12779  ssfzunsnext  12802  fzrevral2  12843  fzshftral  12845  fz0fzdiffz0  12866  elfzmlbp  12868  elfzo  12890  nelfzo  12893  fzoaddel2  12943  fzosubel2  12947  elfzom1p1elfzo  12967  ssfzo12bi  12982  fzonfzoufzol  12990  subfzo0  13009  flltdivnn0lt  13053  modmulnn  13107  modcyc  13124  modaddabs  13127  modaddmod  13128  modmuladd  13131  modadd2mod  13139  modsubmod  13147  modsubmodmod  13148  modaddmodup  13152  modmulmod  13154  modsubdir  13158  modfzo0difsn  13161  modsumfzodifsn  13162  uzindi  13200  axdc4uzlem  13201  expneg2  13288  expdiv  13330  expubnd  13391  mulbinom2  13434  bernneq2  13441  expnngt1  13452  hashinfxadd  13594  hashunsngx  13602  hashunsnggt  13603  hashdifsnp1  13700  ccatval3  13777  ccatsymb  13780  ccatfv0  13781  ccatval1lsw  13782  ccats1val2  13825  swrdnd  13852  pfxsuffeqwrdeq  13896  pfxsuff1eqwrdeq  13897  ccatpfx  13899  swrdswrd  13903  pfxpfx  13906  wrd2ind  13921  swrdccatin1  13923  pfxccatin12lem1  13926  swrdccatin2  13927  pfxccatin12lem3  13930  swrdccat  13933  pfxccatpfx1  13934  pfxccatpfx2  13935  swrdccat3blem  13937  repswswrd  13982  repswpfx  13983  repswccat  13984  cshwidxmod  14001  2cshw  14011  3cshw  14016  scshwfzeqfzo  14024  cshwcsh2id  14026  cshimadifsn  14027  cshimadifsn0  14028  ccatco  14033  cshco  14034  swrdco  14035  pfxco  14036  lswco  14037  swrds2  14138  2swrd2eqwrdeq  14151  shftuz  14262  abs3dif  14525  fsumdifsnconst  14979  modfsummods  14981  sin02gt0  15378  dvdsval2  15443  dvdscmul  15469  dvdsmulc  15470  dvdscmulr  15471  dvdsmulcr  15472  divalglem8  15584  ndvdssub  15593  rpmulgcd  15735  coprmprod  15834  cncongr1  15840  cncongr2  15841  isprm3  15856  modprm0  15971  coprimeprodsq  15974  pythagtriplem12  15992  pythagtriplem14  15994  pcprendvds  16006  pcmul  16017  pcdiv  16018  pcqcl  16022  pcqdiv  16023  pcdvdsb  16034  vdwnnlem1  16160  hashbcss  16169  cshwshashlem1  16258  fvsetsid  16344  setsstruct2  16350  setsstruct  16352  mrcss  16716  mrcsscl  16720  mrcun  16722  cofulid  16989  catcisolem  17195  funcsetcestrclem9  17242  latleeqj1  17502  lubun  17562  clatleglb  17565  pslem  17645  dirtr  17675  mgmb1mgm1  17693  pwspjmhm  17807  grpinvid1  17911  grpinvid2  17912  grpasscan1  17919  grpasscan2  17920  grpinvadd  17934  grpsubf  17935  grpsubrcan  17937  grpinvsub  17938  grpsubeq0  17942  grpsubadd0sub  17943  grppncan  17947  grpnpcan  17948  mulgnn0p1  17994  mulgaddcomlem  18004  mulginvcom  18006  mulginvinv  18007  subgsubcl  18044  subgsub  18045  eqglact  18084  qussub  18093  ghmsub  18107  psgnunilem4  18356  oddvds2  18423  odsubdvds  18426  gexnnod  18443  slwn0  18470  dvrcl  19126  unitdvcl  19127  dvrcan1  19131  dvrcan3  19132  dvreq1  19133  subrgdv  19242  abvsubtri  19296  idsrngd  19323  lmodvsubval2  19379  lsmcl  19545  lsmsp2  19549  lspsntrim  19560  lidldvgen  19717  ascldimul  19804  mpfsubrg  19999  ply1tmcl  20123  eqcoe1ply1eq  20148  gsummoncoe1  20155  lply1binomsc  20158  chrcong  20358  zndvds  20378  zntoslem  20385  ocvsscon  20501  obselocv  20554  frlmphl  20607  mamudm  20681  mamufacex  20682  scmatf1  20824  scmatf1o  20825  scmatrngiso  20829  submabas  20871  mdetdiaglem  20891  mdetralt2  20902  mdetero  20903  mdetunilem2  20906  mdetunilem6  20910  m2detleiblem7  20920  maducoeval2  20933  gsummatr01lem3  20950  gsummatr01  20952  smadiadetglem2  20965  cramerlem1  20980  mply1topmatcl  21097  mp2pm2mplem4  21101  ntrin  21353  elnei  21403  neindisj2  21415  ordtopn3  21488  leordtval2  21504  lecldbas  21511  cnrest2  21578  cmpsublem  21691  ptrescn  21931  xkococn  21952  kqfeq  22016  snfbas  22158  neifil  22172  fclsrest  22316  utopsnnei  22541  neipcfilu  22588  psmetsym  22603  psmetge0  22605  xmetge0  22637  xmetsym  22640  metustto  22846  metustbl  22859  restmetu  22863  nm2dif  22917  nmtri  22918  cnmet  23063  cnmpopc  23215  iihalf1  23218  iihalf2  23220  iocopnst  23227  clmnegsubdi2  23392  clmsub4  23393  clmvsubval2  23397  ncvspi  23443  cphsqrtcl3  23474  cph2ass  23500  cphipval2  23527  cphipval  23529  caublcls  23595  bcthlem3  23612  bcthlem4  23613  srabn  23646  cssbn  23661  cmslsschl  23663  rrxmet  23694  rrxdsfi  23697  iblconst  24101  tdeglem3  24336  mdegmullem  24355  dvdsq1p  24437  coeid3  24513  aannenlem2  24601  pserdvlem2  24699  tanord1  24802  cxpef  24929  recxpcl  24939  logbchbase  25030  relogbcl  25032  relogbzcl  25033  logbleb  25042  logblt  25043  relogbcxpb  25046  lawcos  25075  pythag  25076  isosctrlem1  25077  isosctrlem2  25078  lgsmodeq  25600  lgsmulsqcoprm  25601  gausslemma2dlem1a  25623  2lgsoddprmlem2  25667  ax5seglem1  26397  axcontlem2  26434  axcontlem8  26440  upgrpredgv  26607  numedglnl  26612  issubgr2  26737  uhgrissubgr  26740  egrsubgr  26742  nbusgrfi  26839  nb3grprlem2  26846  cplgr3v  26900  cusgrsizeindslem  26916  finsumvtxdg2size  27015  rusgrpropadjvtx  27050  upgrwlkvtxedg  27109  usgr2trlncl  27223  uspgrn2crct  27268  crctcshwlkn0lem4  27273  crctcshwlkn0lem5  27274  wwlksnextproplem3  27372  umgr2adedgwlklem  27405  rusgr0edg  27434  clwwlk1loop  27448  clwwlkccatlem  27449  clwlkclwwlklem2a4  27457  clwlkclwwlklem2a  27458  clwwisshclwwslemlem  27473  erclwwlktr  27482  clwwlkel  27507  erclwwlkntr  27532  clwwlknonex2lem2  27569  uhgr3cyclex  27643  umgr3cyclex  27644  eucrctshift  27704  frgr3v  27738  3cyclfrgrrn  27749  frgrwopreglem5a  27774  frgr2wsp1  27793  extwwlkfab  27815  clwwlknonclwlknonf1o  27825  numclwwlk3lem1  27845  numclwwlk5  27851  numclwwlk6  27853  isgrpo  27957  grpoinvid1  27988  grpoinvid2  27989  grpoinvop  27993  grpodivinv  27996  grpoinvdiv  27997  grpodivf  27998  grponpcan  28003  ablonncan  28016  nvmval  28102  nvmval2  28103  nvmfval  28104  nvmul0or  28110  nvpncan2  28113  nvaddsub4  28117  nvmeq0  28118  nvdif  28126  nvpi  28127  nvmtri  28131  nvabs  28132  imsmetlem  28150  ipval2lem3  28165  ipval2  28167  4ipval2  28168  ipval3  28169  nmooge0  28227  blometi  28263  hvaddsub12  28498  hvsubdistr1  28509  hvsubdistr2  28510  hvaddcan2  28531  hvmulcan  28532  hvmulcan2  28533  hvsubcan  28534  hvsubcan2  28535  his7  28550  his2sub  28552  his2sub2  28553  norm3dif2  28611  shsubcl  28680  hhssnv  28724  shlej2  28821  fh2  29079  cm2j  29080  pjoi0  29177  hodcl  29207  hosubdi  29268  unopf1o  29376  unopadj  29379  adj2  29394  braadd  29405  bramul  29406  lnopaddmuli  29433  lnopsubmuli  29435  homco2  29437  lnfnaddmuli  29505  adjlnop  29546  leopmul  29594  leoptr  29597  pjimai  29636  atcv1  29840  atexch  29841  atcvatlem  29845  fcoinvbr  30040  divnumden2  30210  xdivmul  30277  cshf1o  30302  dvdschrmulg  30504  resvsca  30549  hasheuni  30953  difelsiga  31001  cndprobin  31301  bayesth  31306  sgn3da  31408  breprexplemc  31512  hashfundm  31960  hashf1dmcdm  31962  lediv2aALT  32522  fununiq  32614  dfrdg2  32643  sltres  32772  sletr  32840  clsun  33279  neiin  33283  rdgeqoa  34195  curfv  34416  matunitlindflem1  34432  poimirlem32  34468  ftc1anclem4  34514  areacirc  34531  filbcmb  34560  ismtybnd  34630  grpoeqdivid  34704  ghomco  34714  rngonegrmul  34767  zerdivemp1x  34770  rngohomco  34797  rngoisoco  34805  riscer  34811  intidl  34852  isfldidl  34891  brredunds  35405  lshpnelb  35664  opnlen0  35868  opcon3b  35876  opcon2b  35877  oplecon3b  35880  opltcon3b  35884  opltcon2b  35886  oldmm1  35897  oldmm4  35900  oldmj1  35901  oldmj4  35904  cvrval2  35954  cvrcon3b  35957  leatb  35972  atcmp  35991  atcvreq0  35994  atlatle  36000  athgt  36136  3dim2  36148  islln2a  36197  lplnnleat  36222  lvolnleat  36263  4atlem10  36286  4atlem11  36289  4atlem12  36292  dalem21  36374  dalem22  36375  dalem23  36376  dalem29  36381  dalem30  36382  dalem31N  36383  dalem32  36384  dalem33  36385  dalem34  36386  dalem35  36387  dalem36  36388  dalem37  36389  dalem40  36392  dalem46  36398  dalem47  36399  dalem51  36403  dalem52  36404  dalem58  36410  dalem59  36411  pmaple  36441  paddclN  36522  pmapjoin  36532  pmapjat1  36533  elpcliN  36573  pclssN  36574  pclun2N  36579  2polcon4bN  36598  paddunN  36607  poldmj1N  36608  pmapj2N  36609  pmapocjN  36610  psubclinN  36628  paddatclN  36629  poml4N  36633  lautco  36777  ldilco  36796  ltrneq2  36828  trljat1  36846  cdlemc1  36871  cdleme10  36934  ltrnco  37399  trlcocnv  37400  trljco  37420  trljco2  37421  cdlemi1  37498  tendocnv  37701  diaord  37727  dibord  37839  dihord3  37937  dihord4  37938  dihmeetlem2N  37979  dihmeetlem4preN  37986  dochdmj1  38070  hdmap10lem  38519  dvdsexpim  38716  expgcd  38718  zexpgcd  38720  readdsub  38750  renpncan3  38755  reppncan  38757  resubdi  38760  mzprename  38844  dvdsrabdioph  38905  pell14qrdivcl  38960  monotoddzz  39038  jm2.19lem2  39085  jm2.19  39088  relexpaddss  39561  k0004lem3  39997  dvconstbi  40217  chordthmALT  40819  isosctrlem1ALT  40820  ssinc  40905  ssdec  40906  unima  40975  wessf1ornlem  40998  disjf1o  41005  disjinfi  41007  ssnnf1octb  41009  projf1o  41012  mapssbi  41029  iunmapsn  41033  upbdrech  41126  iuneqfzuzlem  41156  suplesup  41161  rexabslelem  41247  climxrrelem  41585  limsupresxr  41602  liminfresxr  41603  liminfvalxr  41619  xlimliminflimsup  41698  cncfshift  41712  cncfperiod  41717  cncfuni  41724  icccncfext  41725  dvmptfprodlem  41784  dvnprodlem1  41786  itgspltprt  41819  ismbl3  41827  stoweidlem3  41844  stoweidlem10  41851  stoweidlem19  41860  stoweidlem31  41872  stoweidlem34  41875  stoweidlem44  41885  fourierdlem41  41989  fourierdlem42  41990  fourierdlem51  41998  fourierdlem68  42015  fourierdlem89  42036  fourierdlem91  42038  fourierdlem92  42039  fourierdlem94  42041  etransclem24  42099  etransclem34  42109  qndenserrnbllem  42135  salincl  42164  saldifcl2  42167  subsalsal  42198  sge0pr  42232  sge0pnffigt  42234  sge0reuz  42285  nnfoctbdjlem  42293  nnfoctbdj  42294  meadjiunlem  42303  caratheodorylem2  42365  hoidmv1le  42432  hoidmvlelem3  42435  hspmbllem2  42465  opnvonmbllem2  42471  sssmf  42571  smfaddlem1  42595  sigaraf  42666  sigarmf  42667  nltle2tri  43043  subsubelfzo0  43056  iccpartiltu  43078  icceuelpart  43092  poprelb  43182  reuopreuprim  43184  proththd  43275  mogoldbblem  43381  fppr2odd  43392  fpprel2  43402  bgoldbtbndlem2  43467  isomgrtr  43500  nn0sumltlt  43890  invginvrid  43909  ply1sclrmsm  43931  linccl  43963  lincvalpr  43967  lincresunit3lem1  44028  lincresunit3  44030  fdivmpt  44095  nnolog2flm1  44145  dignnld  44158  digexp  44162  dignn0flhalflem1  44170  reorelicc  44192  eenglngeehlnmlem1  44219  line2  44234  line2xlem  44235  itsclc0lem1  44238  itsclc0xyqsolr  44251  setrec2fun  44289  reccot  44351  rectan  44352