Theorem 3adant2 1131

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

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

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  3ad2ant1  1133  3simpb  1149  3imp3i2an  1346  eupickb  2635  eqeu  3664  onunel  6424  iotan0  6482  funopg  6526  dff1o2  6779  fvelimad  6901  unima  6909  fnimapr  6917  fvmptt  6961  fnreseql  6993  xpprsng  7085  f1elima  7209  f1ounsn  7218  f13dfv  7220  f1ocnvfvb  7225  f1cdmsn  7228  f1ofvswap  7252  oprssov  7527  resf1extb  7876  resf1ext2b  7877  funelss  7991  poxp  8070  poxp2  8085  poxp3  8092  smoiso  8294  oaord  8474  oaword  8476  omcan  8496  omwordri  8499  odi  8506  omeulem1  8509  oeord  8516  oecan  8517  oewordri  8520  oeordsuc  8522  nnaord  8547  nnaordr  8548  nndi  8551  nnaword  8555  nnmwordri  8564  naddel2  8616  naddss1  8617  naddss2  8618  erov  8751  ecopovtrn  8757  mapsnd  8824  f1dom3g  8904  xpdom3  9003  mapxpen  9071  dif1en  9086  findcard  9088  f1domfi2  9106  entrfir  9115  domtrfil  9116  domtrfir  9118  sbthfilem  9122  sdomdomtrfi  9125  php3  9133  findcard3  9183  indexfi  9260  suppr  9375  infpr  9408  r111  9687  tcrank  9796  acndom  9961  infdif2  10119  infxpdom  10120  cfeq0  10166  cfsuc  10167  cfflb  10169  cflim2  10173  cfsmolem  10180  axcc3  10348  domtriomlem  10352  axdc3lem2  10361  axdc3lem4  10363  axdc4lem  10365  axcclem  10367  pwcfsdom  10494  tsktrss  10672  tsksuc  10673  tskuni  10694  adderpqlem  10865  mulerpqlem  10866  mulcanenq  10871  distrnq  10872  ltsonq  10880  ltanq  10882  ltmnq  10883  distrlem1pr  10936  distrlem5pr  10938  ltsopr  10943  ltsosr  11005  ltasr  11011  adddir  11123  axlttrn  11205  letr  11227  nnncan1  11417  npncan3  11419  pnpcan2  11421  subdi  11570  subdir  11571  mulcan1g  11790  mulcan2g  11791  divmul  11799  div23  11815  div13  11817  muldivdir  11834  divsubdir  11835  subdivcomb1  11836  divcan7  11850  ltmul2  11992  lemul1  11993  lemul2  11994  lemul2a  11996  lediv1  12007  ltmuldiv2  12016  lemuldiv  12022  lemuldiv2  12023  ltdiv2  12028  lediv2  12032  infrelb  12127  nndivtr  12192  bndndx  12400  nn0n0n1ge2  12469  fnn0ind  12591  addlelt  13021  xrletr  13072  qsqueeze  13116  xleadd2a  13169  xleadd1  13170  xltadd2  13172  xltmul2  13208  supxrbnd  13243  iooneg  13387  iccneg  13388  icoshft  13389  icoshftf1o  13390  zltaddlt1le  13421  fzen  13457  uzsubsubfz  13462  ssfzunsnext  13485  fzrevral2  13529  fzshftral  13531  fz0fzdiffz0  13553  elfzmlbp  13555  elfzo  13577  nelfzo  13580  fzoaddel2  13636  fzosubel2  13641  ssfzo12bi  13677  fzonfzoufzol  13687  subfzo0  13708  flltdivnn0lt  13753  modmulnn  13809  modcyc  13826  modaddabs  13831  modaddmod  13832  modmuladd  13836  modadd2mod  13844  modsubmod  13852  modsubmodmod  13853  modaddmodup  13857  modmulmod  13859  modsubdir  13863  modfzo0difsn  13866  modsumfzodifsn  13867  uzindi  13905  axdc4uzlem  13906  expneg2  13993  expdiv  14036  expubnd  14101  mulbinom2  14146  bernneq2  14153  expnngt1  14164  hashinfxadd  14308  hashunsngx  14316  hashunsnggt  14317  hashfundm  14365  hashf1dmcdm  14367  hashdifsnp1  14429  ccatval3  14502  ccatfv0  14507  ccatval1lsw  14508  ccats1val2  14551  ccatw2s1p1  14560  swrdnd  14578  pfxsuffeqwrdeq  14621  pfxsuff1eqwrdeq  14622  swrdswrd  14628  pfxpfx  14631  wrd2ind  14646  swrdccatin1  14648  pfxccatin12lem1  14651  swrdccatin2  14652  pfxccatin12lem3  14655  swrdccat  14658  pfxccatpfx1  14659  pfxccatpfx2  14660  swrdccat3blem  14662  repswswrd  14707  repswpfx  14708  repswccat  14709  cshwidxmod  14726  2cshw  14736  3cshw  14741  scshwfzeqfzo  14749  cshwcsh2id  14751  cshimadifsn  14752  cshimadifsn0  14753  ccatco  14758  cshco  14759  swrdco  14760  pfxco  14761  lswco  14762  swrds2  14863  2swrd2eqwrdeq  14876  shftuz  14992  abs3dif  15255  fsumdifsnconst  15714  modfsummods  15716  sin02gt0  16117  dvdsval2  16182  dvdscmul  16209  dvdsmulc  16210  dvdscmulr  16211  dvdsmulcr  16212  divalglem8  16327  ndvdssub  16336  dvdsexpim  16482  rpmulgcd  16484  expgcd  16490  zexpgcd  16492  coprmprod  16588  cncongr1  16594  cncongr2  16595  isprm3  16610  modprm0  16733  coprimeprodsq  16736  pythagtriplem12  16754  pythagtriplem14  16756  pcprendvds  16768  pcmul  16779  pcdiv  16780  pcqcl  16784  pcqdiv  16785  pcdvdsb  16797  vdwnnlem1  16923  hashbcss  16932  cshwshashlem1  17023  fvsetsid  17095  setsstruct2  17101  setsstruct  17103  mrcss  17539  mrcsscl  17543  mrcun  17545  cofulid  17814  catcisolem  18034  funcsetcestrclem9  18086  latleeqj1  18374  lubun  18438  clatleglb  18441  pslem  18495  dirtr  18525  mgmb1mgm1  18580  pwspjmhm  18755  grpinvid1  18921  grpinvid2  18922  grpasscan1  18931  grpasscan2  18932  grpinvadd  18948  grpsubf  18949  grpsubrcan  18951  grpinvsub  18952  grpsubeq0  18956  grpsubadd0sub  18957  grppncan  18961  grpnpcan  18962  mulgnn0p1  19015  mulgaddcomlem  19027  mulginvcom  19029  mulginvinv  19030  subgsubcl  19067  subgsub  19068  eqglact  19108  qussub  19120  ghmsub  19153  psgnunilem4  19426  oddvds2  19495  odsubdvds  19500  gexnnod  19517  slwn0  19544  dvrcl  20340  unitdvcl  20341  dvrcan1  20345  dvrcan3  20346  dvreq1  20347  rngisom1  20402  rngisomring  20403  subrgdv  20522  abvsubtri  20760  idsrngd  20789  lmodvsubval2  20868  lsmcl  21035  lsmsp2  21039  lspsntrim  21050  rngqiprngimfolem  21245  lidldvgen  21289  cncrng  21343  chrcong  21482  dvdschrmulg  21483  zndvds  21504  zntoslem  21511  ocvsscon  21630  obselocv  21683  frlmphl  21736  ascldimul  21844  mpfsubrg  22066  ply1tmcl  22214  eqcoe1ply1eq  22243  gsummoncoe1  22252  lply1binomsc  22255  mamudm  22339  mamufacex  22340  scmatf1  22475  scmatf1o  22476  scmatrngiso  22480  submabas  22522  mdetdiaglem  22542  mdetralt2  22553  mdetero  22554  mdetunilem2  22557  mdetunilem6  22561  m2detleiblem7  22571  maducoeval2  22584  gsummatr01lem3  22601  gsummatr01  22603  smadiadetglem2  22616  cramerlem1  22631  mply1topmatcl  22749  mp2pm2mplem4  22753  ntrin  23005  elnei  23055  neindisj2  23067  ordtopn3  23140  leordtval2  23156  lecldbas  23163  cnrest2  23230  cmpsublem  23343  ptrescn  23583  xkococn  23604  kqfeq  23668  snfbas  23810  neifil  23824  fclsrest  23968  utopsnnei  24193  neipcfilu  24239  psmetsym  24254  psmetge0  24256  xmetge0  24288  xmetsym  24291  metustto  24497  metustbl  24510  restmetu  24514  nm2dif  24569  nmtri  24570  cnmet  24715  cnmpopc  24878  iihalf1  24881  iihalf2  24884  iocopnst  24893  clmnegsubdi2  25061  clmsub4  25062  clmvsubval2  25066  ncvspi  25112  cphsqrtcl3  25143  cph2ass  25169  cphipval2  25197  cphipval  25199  caublcls  25265  bcthlem3  25282  bcthlem4  25283  srabn  25316  cssbn  25331  cmslsschl  25333  rrxmet  25364  rrxdsfi  25367  iblconst  25775  dvdsq1p  26124  coeid3  26201  aannenlem2  26293  pserdvlem2  26394  tanord1  26502  cxpef  26630  recxpcl  26640  logbchbase  26737  relogbcl  26739  relogbzcl  26740  logbleb  26749  logblt  26750  relogbcxpb  26753  lawcos  26782  pythag  26783  isosctrlem1  26784  isosctrlem2  26785  lgsmodeq  27309  lgsmulsqcoprm  27310  gausslemma2dlem1a  27332  2lgsoddprmlem2  27376  ltsres  27630  lestr  27730  cofcutr  27920  lrrecpo  27937  ltadds2im  27982  leadds2im  27984  leadds1  27985  leadds2  27986  ltadds1  27988  addscan2  27989  addscan1  27990  ltsubs1  28072  divmulsw  28189  oldfib  28373  zsoring  28405  bdayfinbndlem1  28463  ax5seglem1  29001  axcontlem2  29038  axcontlem8  29044  upgrpredgv  29212  numedglnl  29217  issubgr2  29345  uhgrissubgr  29348  egrsubgr  29350  nbusgrfi  29447  nb3grprlem2  29454  cplgr3v  29508  cusgrsizeindslem  29525  finsumvtxdg2size  29624  rusgrpropadjvtx  29659  upgrwlkvtxedg  29718  usgr2trlncl  29833  uspgrn2crct  29881  crctcshwlkn0lem4  29886  crctcshwlkn0lem5  29887  wwlksnextproplem3  29984  umgr2adedgwlklem  30017  rusgr0edg  30049  clwwlk1loop  30063  clwwlkccatlem  30064  clwlkclwwlklem2a4  30072  clwlkclwwlklem2a  30073  clwwisshclwwslemlem  30088  erclwwlktr  30097  clwwlkel  30121  erclwwlkntr  30146  clwwlknonex2lem2  30183  uhgr3cyclex  30257  umgr3cyclex  30258  eucrctshift  30318  frgr3v  30350  3cyclfrgrrn  30361  frgrwopreglem5a  30386  frgr2wsp1  30405  extwwlkfab  30427  clwwlknonclwlknonf1o  30437  numclwwlk3lem1  30457  numclwwlk5  30463  numclwwlk6  30465  isgrpo  30572  grpoinvid1  30603  grpoinvid2  30604  grpoinvop  30608  grpodivinv  30611  grpoinvdiv  30612  grpodivf  30613  grponpcan  30618  ablonncan  30631  nvmval  30717  nvmval2  30718  nvmfval  30719  nvmul0or  30725  nvpncan2  30728  nvaddsub4  30732  nvmeq0  30733  nvdif  30741  nvpi  30742  nvmtri  30746  nvabs  30747  imsmetlem  30765  ipval2lem3  30780  ipval2  30782  4ipval2  30783  ipval3  30784  nmooge0  30842  blometi  30878  hvaddsub12  31113  hvsubdistr1  31124  hvsubdistr2  31125  hvaddcan2  31146  hvmulcan  31147  hvmulcan2  31148  hvsubcan  31149  hvsubcan2  31150  his7  31165  his2sub  31167  his2sub2  31168  norm3dif2  31226  shsubcl  31295  hhssnv  31339  shlej2  31436  fh2  31694  cm2j  31695  pjoi0  31792  hodcl  31822  hosubdi  31883  unopf1o  31991  unopadj  31994  adj2  32009  braadd  32020  bramul  32021  lnopaddmuli  32048  lnopsubmuli  32050  homco2  32052  lnfnaddmuli  32120  adjlnop  32161  leopmul  32209  leoptr  32212  pjimai  32251  atcv1  32455  atexch  32456  atcvatlem  32460  fcoinvbr  32680  preiman0  32789  divnumden2  32896  sgn3da  32915  xdivmul  33006  cshf1o  33044  resvsca  33413  idlsrgcmnd  33596  hasheuni  34242  difelsiga  34290  cndprobin  34591  bayesth  34596  signstfvp  34728  breprexplemc  34789  trssfir1om  35267  fineqvac  35272  fineqvnttrclselem1  35277  fineqvnttrclselem3  35279  trssfir1omregs  35292  swrdrevpfx  35311  swrdwlk  35321  lediv2aALT  35871  fununiq  35963  dfrdg2  35987  clsun  36522  neiin  36526  rdgeqoa  37571  curfv  37797  matunitlindflem1  37813  poimirlem32  37849  ftc1anclem4  37893  areacirc  37910  filbcmb  37937  ismtybnd  38004  grpoeqdivid  38078  ghomco  38088  rngonegrmul  38141  zerdivemp1x  38144  rngohomco  38171  rngoisoco  38179  riscer  38185  intidl  38226  isfldidl  38265  eceldmqsxrncnvepres  38617  eceldmqsxrncnvepres2  38618  brredunds  38879  lshpnelb  39240  opnlen0  39444  opcon3b  39452  opcon2b  39453  oplecon3b  39456  opltcon3b  39460  opltcon2b  39462  oldmm1  39473  oldmm4  39476  oldmj1  39477  oldmj4  39480  cvrval2  39530  cvrcon3b  39533  leatb  39548  atcmp  39567  atcvreq0  39570  atlatle  39576  athgt  39712  3dim2  39724  islln2a  39773  lplnnleat  39798  lvolnleat  39839  4atlem10  39862  4atlem11  39865  4atlem12  39868  dalem21  39950  dalem22  39951  dalem23  39952  dalem29  39957  dalem30  39958  dalem31N  39959  dalem32  39960  dalem33  39961  dalem34  39962  dalem35  39963  dalem36  39964  dalem37  39965  dalem40  39968  dalem46  39974  dalem47  39975  dalem51  39979  dalem52  39980  dalem58  39986  dalem59  39987  pmaple  40017  paddclN  40098  pmapjoin  40108  pmapjat1  40109  elpcliN  40149  pclssN  40150  pclun2N  40155  2polcon4bN  40174  paddunN  40183  poldmj1N  40184  pmapj2N  40185  pmapocjN  40186  psubclinN  40204  paddatclN  40205  poml4N  40209  lautco  40353  ldilco  40372  ltrneq2  40404  trljat1  40422  cdlemc1  40447  cdleme10  40510  ltrnco  40975  trlcocnv  40976  trljco  40996  trljco2  40997  cdlemi1  41074  tendocnv  41277  diaord  41303  dibord  41415  dihord3  41513  dihord4  41514  dihmeetlem2N  41555  dihmeetlem4preN  41562  dochdmj1  41646  hdmap10lem  42095  lcmineqlem1  42279  sticksstones2  42397  readdsub  42635  reltsub1  42637  renpncan3  42642  reppncan  42644  resubdi  42647  readdcan2  42664  mzprename  42987  dvdsrabdioph  43048  pell14qrdivcl  43103  monotoddzz  43181  jm2.19lem2  43228  jm2.19  43231  relexpaddss  43955  k0004lem3  44386  dvconstbi  44571  chordthmALT  45169  isosctrlem1ALT  45170  ssinc  45327  ssdec  45328  wessf1ornlem  45425  disjf1o  45431  ssnnf1octb  45434  projf1o  45437  mapssbi  45453  iunmapsn  45457  upbdrech  45549  iuneqfzuzlem  45575  suplesup  45580  rexabslelem  45658  climxrrelem  45989  limsupresxr  46006  liminfresxr  46007  liminfvalxr  46023  xlimliminflimsup  46102  cncfshift  46114  cncfperiod  46119  cncfuni  46126  icccncfext  46127  dvmptfprodlem  46184  dvnprodlem1  46186  itgspltprt  46219  ismbl3  46226  stoweidlem3  46243  stoweidlem10  46250  stoweidlem19  46259  stoweidlem31  46271  stoweidlem34  46274  stoweidlem44  46284  fourierdlem41  46388  fourierdlem42  46389  fourierdlem51  46397  fourierdlem68  46414  fourierdlem89  46435  fourierdlem91  46437  fourierdlem92  46438  fourierdlem94  46440  etransclem24  46498  etransclem34  46508  qndenserrnbllem  46534  salincl  46564  saldifcl2  46568  subsalsal  46599  sge0pr  46634  sge0pnffigt  46636  sge0reuz  46687  nnfoctbdjlem  46695  nnfoctbdj  46696  meadjiunlem  46705  caratheodorylem2  46767  hoidmv1le  46834  hoidmvlelem3  46837  hspmbllem2  46867  opnvonmbllem2  46873  sssmf  46978  smfaddlem1  47003  sigaraf  47093  sigarmf  47094  nltle2tri  47555  subsubelfzo0  47568  submodaddmod  47583  zplusmodne  47585  addmodne  47586  minusmod5ne  47591  submodneaddmod  47593  modmkpkne  47603  modmknepk  47604  iccpartiltu  47664  icceuelpart  47678  poprelb  47766  reuopreuprim  47768  proththd  47856  mogoldbblem  47962  fppr2odd  47973  fpprel2  47983  bgoldbtbndlem2  48048  clnbusgrfi  48085  grimuhgr  48129  uhgrimisgrgric  48173  clnbgrgrim  48176  grtrif1o  48184  grlimgrtri  48245  gpgusgralem  48298  gpgedgvtx0  48303  gpgedg2ov  48308  gpgedg2iv  48309  gpg5nbgrvtx03starlem2  48311  nn0sumltlt  48592  invginvrid  48609  ply1sclrmsm  48626  linccl  48656  lincvalpr  48660  lincresunit3lem1  48721  lincresunit3  48723  fdivmpt  48782  nnolog2flm1  48832  dignnld  48845  digexp  48849  dignn0flhalflem1  48857  itcovalsucov  48910  reorelicc  48952  eenglngeehlnmlem1  48979  line2  48994  line2xlem  48995  itsclc0lem1  48998  itsclc0xyqsolr  49011  i0oii  49161  io1ii  49162  indthinc  49703  indthincALT  49704  setrec2fun  49933  reccot  49999  rectan  50000