Theorem 3adant2 1143

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  3ad2ant1  1145  3simpb  1161  3imp3i2an  1358  eupickb  2661  eqeu  3667  onunel  6447  iotan0  6505  funopg  6549  dff1o2  6806  fvelimad  6928  unima  6936  fnimapr  6944  fvmptt  6990  fnreseql  7023  xpprsng  7116  f1elima  7241  f1ounsn  7250  f13dfv  7252  f1ocnvfvb  7257  f1cdmsn  7260  f1ofvswap  7284  oprssov  7559  resf1extb  7909  resf1ext2b  7910  funelss  8022  poxp  8101  poxp2  8116  poxp3  8123  smoiso  8326  oaord  8509  oaword  8511  omcan  8531  omwordri  8534  odi  8541  omeulem1  8544  oeord  8551  oecan  8552  oewordri  8555  oeordsuc  8557  nnaord  8582  nnaordr  8583  nndi  8586  nnaword  8590  nnmwordri  8599  naddel2  8652  naddss1  8653  naddss2  8654  erov  8789  ecopovtrn  8795  mapsnd  8861  f1dom3g  8941  xpdom3  9040  mapxpen  9108  dif1en  9123  findcard  9125  f1domfi2  9143  entrfir  9152  domtrfil  9153  domtrfir  9155  sbthfilem  9159  sdomdomtrfi  9162  php3  9170  findcard3  9220  indexfi  9296  suppr  9411  infpr  9444  r111  9726  tcrank  9835  acndom  10000  infdif2  10158  infxpdom  10159  cfeq0  10206  cfsuc  10207  cfflb  10209  cflim2  10213  cfsmolem  10220  axcc3  10388  domtriomlem  10392  axdc3lem2  10401  axdc3lem4  10403  axdc4lem  10405  axcclem  10407  pwcfsdom  10534  tsktrss  10712  tsksuc  10713  tskuni  10734  adderpqlem  10905  mulerpqlem  10906  mulcanenq  10911  distrnq  10912  ltsonq  10920  ltanq  10922  ltmnq  10923  distrlem1pr  10976  distrlem5pr  10978  ltsopr  10983  ltsosr  11045  ltasr  11051  adddir  11163  axlttrn  11248  letr  11270  nnncan1  11460  npncan3  11462  pnpcan2  11464  subdi  11613  subdir  11614  mulcan1g  11833  mulcan2g  11834  divmul  11841  div23  11857  div13  11859  muldivdir  11876  divsubdir  11877  subdivcomb1  11879  divcan7  11893  ltmul2  12035  lemul1  12036  lemul2  12037  lemul2a  12039  lediv1  12050  ltmuldiv2  12059  lemuldiv  12065  lemuldiv2  12066  ltdiv2  12071  lediv2  12075  infrelb  12170  nndivtr  12253  bndndx  12473  nn0n0n1ge2  12542  fnn0ind  12665  addlelt  13102  xrletr  13153  qsqueeze  13197  xleadd2a  13250  xleadd1  13251  xltadd2  13253  xltmul2  13289  supxrbnd  13324  iooneg  13468  iccneg  13469  icoshft  13470  icoshftf1o  13471  zltaddlt1le  13502  fzen  13539  uzsubsubfz  13544  ssfzunsnext  13567  fzrevral2  13611  fzshftral  13613  fz0fzdiffz0  13635  elfzmlbp  13637  elfzo  13659  nelfzo  13663  fzoaddel2  13719  fzosubel2  13724  ssfzo12bi  13760  fzonfzoufzol  13770  subfzo0  13791  flltdivnn0lt  13836  modmulnn  13892  modcyc  13909  modaddabs  13914  modaddmod  13915  modmuladd  13919  modadd2mod  13927  modsubmod  13935  modsubmodmod  13936  modaddmodup  13940  modmulmod  13942  modsubdir  13946  modfzo0difsn  13949  modsumfzodifsn  13950  uzindi  13988  axdc4uzlem  13989  expneg2  14076  expdiv  14119  expubnd  14184  mulbinom2  14229  bernneq2  14236  expnngt1  14247  hashinfxadd  14391  hashunsngx  14399  hashunsnggt  14400  hashfundm  14448  hashf1dmcdm  14450  hashdifsnp1  14512  ccatval3  14585  ccatfv0  14590  ccatval1lsw  14591  ccats1val2  14634  ccatw2s1p1  14643  swrdnd  14661  pfxsuffeqwrdeq  14704  pfxsuff1eqwrdeq  14705  swrdswrd  14711  pfxpfx  14714  wrd2ind  14729  swrdccatin1  14731  pfxccatin12lem1  14734  swrdccatin2  14735  pfxccatin12lem3  14738  swrdccat  14741  pfxccatpfx1  14742  pfxccatpfx2  14743  swrdccat3blem  14745  repswswrd  14790  repswpfx  14791  repswccat  14792  cshwidxmod  14809  2cshw  14819  3cshw  14824  scshwfzeqfzo  14832  cshwcsh2id  14834  cshimadifsn  14835  cshimadifsn0  14836  ccatco  14841  cshco  14842  swrdco  14843  pfxco  14844  lswco  14845  swrds2  14946  2swrd2eqwrdeq  14959  shftuz  15075  sgn3da  15104  abs3dif  15349  fsumdifsnconst  15809  modfsummods  15811  sin02gt0  16214  dvdsval2  16279  dvdscmul  16306  dvdsmulc  16307  dvdscmulr  16308  dvdsmulcr  16309  divalglem8  16424  ndvdssub  16433  dvdsexpim  16579  rpmulgcd  16581  expgcd  16587  zexpgcd  16589  coprmprod  16685  cncongr1  16691  cncongr2  16692  isprm3  16707  modprm0  16831  coprimeprodsq  16834  pythagtriplem12  16852  pythagtriplem14  16854  pcprendvds  16866  pcmul  16877  pcdiv  16878  pcqcl  16882  pcqdiv  16883  pcdvdsb  16895  vdwnnlem1  17021  hashbcss  17030  cshwshashlem1  17121  fvsetsid  17194  setsstruct2  17200  setsstruct  17202  mrcss  17638  mrcsscl  17642  mrcun  17644  cofulid  17913  catcisolem  18133  funcsetcestrclem9  18185  latleeqj1  18473  lubun  18537  clatleglb  18540  pslem  18594  dirtr  18624  mgmb1mgm1  18679  pwspjmhm  18854  grpinvid1  19023  grpinvid2  19024  grpasscan1  19033  grpasscan2  19034  grpinvadd  19050  grpsubf  19051  grpsubrcan  19053  grpinvsub  19054  grpsubeq0  19058  grpsubadd0sub  19059  grppncan  19063  grpnpcan  19064  mulgnn0p1  19117  mulgaddcomlem  19129  mulginvcom  19131  mulginvinv  19132  subgsubcl  19169  subgsub  19170  eqglact  19210  qussub  19222  ghmsub  19254  psgnunilem4  19527  oddvds2  19596  odsubdvds  19601  gexnnod  19618  slwn0  19645  dvrcl  20439  unitdvcl  20440  dvrcan1  20444  dvrcan3  20445  dvreq1  20446  rngisom1  20501  rngisomring  20502  subrgdv  20625  abvsubtri  20863  idsrngd  20892  lmodvsubval2  20971  lsmcl  21137  lsmsp2  21141  lspsntrim  21152  rngqiprngimfolem  21347  lidldvgen  21391  cncrng  21432  chrcong  21566  dvdschrmulg  21567  zndvds  21588  zntoslem  21595  ocvsscon  21714  obselocv  21767  frlmphl  21820  ascldimul  21927  mpfsubrg  22151  ply1tmcl  22322  eqcoe1ply1eq  22349  gsummoncoe1  22358  lply1binomsc  22361  mamudm  22442  mamufacex  22443  scmatf1  22578  scmatf1o  22579  scmatrngiso  22583  submabas  22625  mdetdiaglem  22645  mdetralt2  22656  mdetero  22657  mdetunilem2  22660  mdetunilem6  22664  m2detleiblem7  22674  maducoeval2  22687  gsummatr01lem3  22704  gsummatr01  22706  smadiadetglem2  22719  cramerlem1  22734  mply1topmatcl  22852  mp2pm2mplem4  22856  ntrin  23108  elnei  23158  neindisj2  23170  ordtopn3  23243  leordtval2  23259  lecldbas  23266  cnrest2  23333  cmpsublem  23446  ptrescn  23686  xkococn  23707  kqfeq  23771  snfbas  23913  neifil  23927  fclsrest  24071  utopsnnei  24296  neipcfilu  24342  psmetsym  24357  psmetge0  24359  xmetge0  24391  xmetsym  24394  metustto  24600  metustbl  24613  restmetu  24617  nm2dif  24672  nmtri  24673  cnmet  24818  cnmpopc  24977  iihalf1  24980  iihalf2  24982  iocopnst  24989  clmnegsubdi2  25154  clmsub4  25155  clmvsubval2  25159  ncvspi  25205  cphsqrtcl3  25236  cph2ass  25262  cphipval2  25290  cphipval  25292  caublcls  25358  bcthlem3  25375  bcthlem4  25376  srabn  25409  cssbn  25424  cmslsschl  25426  rrxmet  25457  rrxdsfi  25460  iblconst  25867  dvdsq1p  26210  coeid3  26287  aannenlem2  26380  pserdvlem2  26478  tanord1  26589  cxpef  26717  recxpcl  26727  logbchbase  26823  relogbcl  26825  relogbzcl  26826  logbleb  26835  logblt  26836  relogbcxpb  26839  lawcos  26868  pythag  26869  isosctrlem1  26870  isosctrlem2  26871  lgsmodeq  27393  lgsmulsqcoprm  27394  gausslemma2dlem1a  27416  2lgsoddprmlem2  27460  ltsres  27713  lestr  27813  cofcutr  28004  lrrecpo  28021  ltadds2im  28066  leadds2im  28068  leadds1  28069  leadds2  28070  ltadds1  28072  addscan2  28073  addscan1  28074  ltsubs1  28156  divmulsw  28273  oldfib  28457  zsoring  28489  bdayfinbndlem1  28547  ax5seglem1  29085  axcontlem2  29122  axcontlem8  29128  upgrpredgv  29296  numedglnl  29301  issubgr2  29429  uhgrissubgr  29432  egrsubgr  29434  nbusgrfi  29531  nb3grprlem2  29538  cplgr3v  29592  cusgrsizeindslem  29608  finsumvtxdg2size  29707  rusgrpropadjvtx  29742  upgrwlkvtxedg  29801  usgr2trlncl  29916  uspgrn2crct  29964  crctcshwlkn0lem4  29969  crctcshwlkn0lem5  29970  wwlksnextproplem3  30067  umgr2adedgwlklem  30100  rusgr0edg  30132  clwwlk1loop  30146  clwwlkccatlem  30147  clwlkclwwlklem2a4  30155  clwlkclwwlklem2a  30156  clwwisshclwwslemlem  30171  erclwwlktr  30180  clwwlkel  30204  erclwwlkntr  30229  clwwlknonex2lem2  30266  uhgr3cyclex  30340  umgr3cyclex  30341  eucrctshift  30401  frgr3v  30433  3cyclfrgrrn  30444  frgrwopreglem5a  30469  frgr2wsp1  30488  extwwlkfab  30510  clwwlknonclwlknonf1o  30520  numclwwlk3lem1  30540  numclwwlk5  30546  numclwwlk6  30548  isgrpo  30656  grpoinvid1  30687  grpoinvid2  30688  grpoinvop  30692  grpodivinv  30695  grpoinvdiv  30696  grpodivf  30697  grponpcan  30702  ablonncan  30715  nvmval  30801  nvmval2  30802  nvmfval  30803  nvmul0or  30809  nvpncan2  30812  nvaddsub4  30816  nvmeq0  30817  nvdif  30825  nvpi  30826  nvmtri  30830  nvabs  30831  imsmetlem  30849  ipval2lem3  30864  ipval2  30866  4ipval2  30867  ipval3  30868  nmooge0  30926  blometi  30962  hvaddsub12  31197  hvsubdistr1  31208  hvsubdistr2  31209  hvaddcan2  31230  hvmulcan  31231  hvmulcan2  31232  hvsubcan  31233  hvsubcan2  31234  his7  31249  his2sub  31251  his2sub2  31252  norm3dif2  31310  shsubcl  31379  hhssnv  31423  shlej2  31520  fh2  31778  cm2j  31779  pjoi0  31876  hodcl  31906  hosubdi  31967  unopf1o  32075  unopadj  32078  adj2  32093  braadd  32104  bramul  32105  lnopaddmuli  32132  lnopsubmuli  32134  homco2  32136  lnfnaddmuli  32204  adjlnop  32245  leopmul  32293  leoptr  32296  pjimai  32335  atcv1  32539  atexch  32540  atcvatlem  32544  fcoinvbr  32764  preiman0  32872  divnumden2  32978  xdivmul  33062  cshf1o  33100  resvsca  33478  idlsrgcmnd  33671  hasheuni  34342  difelsiga  34390  cndprobin  34691  bayesth  34696  signstfvp  34825  breprexplemc  34886  trssfir1om  35367  fineqvac  35372  fineqvnttrclselem1  35377  fineqvnttrclselem3  35379  trssfir1omregs  35392  swrdrevpfx  35427  swrdwlk  35437  lediv2aALT  35987  fununiq  36079  dfrdg2  36103  clsun  36648  neiin  36652  rdgeqoa  37824  curfv  38059  matunitlindflem1  38075  poimirlem32  38111  ftc1anclem4  38155  areacirc  38172  filbcmb  38199  ismtybnd  38266  grpoeqdivid  38340  ghomco  38350  rngonegrmul  38403  zerdivemp1x  38406  rngohomco  38433  rngoisoco  38441  riscer  38447  intidl  38488  isfldidl  38527  eceldmqsxrncnvepres  38895  eceldmqsxrncnvepres2  38896  brredunds  39169  lshpnelb  39568  opnlen0  39772  opcon3b  39780  opcon2b  39781  oplecon3b  39784  opltcon3b  39788  opltcon2b  39790  oldmm1  39801  oldmm4  39804  oldmj1  39805  oldmj4  39808  cvrval2  39858  cvrcon3b  39861  leatb  39876  atcmp  39895  atcvreq0  39898  atlatle  39904  athgt  40040  3dim2  40052  islln2a  40101  lplnnleat  40126  lvolnleat  40167  4atlem10  40190  4atlem11  40193  4atlem12  40196  dalem21  40278  dalem22  40279  dalem23  40280  dalem29  40285  dalem30  40286  dalem31N  40287  dalem32  40288  dalem33  40289  dalem34  40290  dalem35  40291  dalem36  40292  dalem37  40293  dalem40  40296  dalem46  40302  dalem47  40303  dalem51  40307  dalem52  40308  dalem58  40314  dalem59  40315  pmaple  40345  paddclN  40426  pmapjoin  40436  pmapjat1  40437  elpcliN  40477  pclssN  40478  pclun2N  40483  2polcon4bN  40502  paddunN  40511  poldmj1N  40512  pmapj2N  40513  pmapocjN  40514  psubclinN  40532  paddatclN  40533  poml4N  40537  lautco  40681  ldilco  40700  ltrneq2  40732  trljat1  40750  cdlemc1  40775  cdleme10  40838  ltrnco  41303  trlcocnv  41304  trljco  41324  trljco2  41325  cdlemi1  41402  tendocnv  41605  diaord  41631  dibord  41743  dihord3  41841  dihord4  41842  dihmeetlem2N  41883  dihmeetlem4preN  41890  dochdmj1  41974  hdmap10lem  42423  lcmineqlem1  42606  sticksstones2  42724  readdsub  42953  reltsub1  42955  renpncan3  42960  reppncan  42962  resubdi  42965  readdcan2  42982  mzprename  43290  dvdsrabdioph  43347  pell14qrdivcl  43402  monotoddzz  43480  jm2.19lem2  43527  jm2.19  43530  relexpaddss  44254  k0004lem3  44685  dvconstbi  44870  chordthmALT  45468  isosctrlem1ALT  45469  ssinc  45625  ssdec  45626  wessf1ornlem  45723  disjf1o  45729  ssnnf1octb  45732  projf1o  45734  mapssbi  45749  iunmapsn  45753  upbdrech  45844  iuneqfzuzlem  45870  suplesup  45875  rexabslelem  45952  climxrrelem  46283  limsupresxr  46300  liminfresxr  46301  liminfvalxr  46317  xlimliminflimsup  46396  cncfshift  46408  cncfperiod  46413  cncfuni  46420  icccncfext  46421  dvmptfprodlem  46478  dvnprodlem1  46480  itgspltprt  46513  ismbl3  46520  stoweidlem3  46537  stoweidlem10  46544  stoweidlem19  46553  stoweidlem31  46565  stoweidlem34  46568  stoweidlem44  46578  fourierdlem41  46682  fourierdlem42  46683  fourierdlem51  46691  fourierdlem68  46708  fourierdlem89  46729  fourierdlem91  46731  fourierdlem92  46732  fourierdlem94  46734  etransclem24  46792  etransclem34  46802  qndenserrnbllem  46828  salincl  46858  saldifcl2  46862  subsalsal  46893  sge0pr  46928  sge0pnffigt  46930  sge0reuz  46981  nnfoctbdjlem  46989  nnfoctbdj  46990  meadjiunlem  46999  caratheodorylem2  47061  hoidmv1le  47128  hoidmvlelem3  47131  hspmbllem2  47161  opnvonmbllem2  47167  smfaddlem1  47297  sigaraf  47387  sigarmf  47388  nltle2tri  47867  subsubelfzo0  47881  nnmul2  47884  submodaddmod  47901  zplusmodne  47903  addmodne  47904  minusmod5ne  47909  submodneaddmod  47911  modmkpkne  47921  modmknepk  47922  iccpartiltu  47988  icceuelpart  48002  poprelb  48090  reuopreuprim  48092  nprmmul2  48094  proththd  48183  mogoldbblem  48302  fppr2odd  48313  fpprel2  48323  bgoldbtbndlem2  48388  clnbusgrfi  48425  grimuhgr  48469  uhgrimisgrgric  48513  clnbgrgrim  48516  grtrif1o  48524  grlimgrtri  48585  gpgusgralem  48638  gpgedgvtx0  48643  gpgedg2ov  48648  gpgedg2iv  48649  gpg5nbgrvtx03starlem2  48651  nn0sumltlt  48932  invginvrid  48949  ply1sclrmsm  48966  linccl  48996  lincvalpr  49000  lincresunit3lem1  49061  lincresunit3  49063  fdivmpt  49122  nnolog2flm1  49172  dignnld  49185  digexp  49189  dignn0flhalflem1  49197  itcovalsucov  49250  reorelicc  49292  eenglngeehlnmlem1  49319  line2  49334  line2xlem  49335  itsclc0lem1  49338  itsclc0xyqsolr  49351  i0oii  49501  io1ii  49502  indthinc  50043  indthincALT  50044  setrec2fun  50273  reccot  50339  rectan  50340