Theorem 3adant2 1132

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

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

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 1089

This theorem is referenced by:  3ad2ant1  1134  3simpb  1150  3imp3i2an  1347  eupickb  2636  eqeu  3653  onunel  6424  iotan0  6482  funopg  6526  dff1o2  6779  fvelimad  6901  unima  6909  fnimapr  6917  fvmptt  6962  fnreseql  6994  xpprsng  7087  f1elima  7211  f1ounsn  7220  f13dfv  7222  f1ocnvfvb  7227  f1cdmsn  7230  f1ofvswap  7254  oprssov  7529  resf1extb  7878  resf1ext2b  7879  funelss  7993  poxp  8071  poxp2  8086  poxp3  8093  smoiso  8295  oaord  8475  oaword  8477  omcan  8497  omwordri  8500  odi  8507  omeulem1  8510  oeord  8517  oecan  8518  oewordri  8521  oeordsuc  8523  nnaord  8548  nnaordr  8549  nndi  8552  nnaword  8556  nnmwordri  8565  naddel2  8617  naddss1  8618  naddss2  8619  erov  8754  ecopovtrn  8760  mapsnd  8827  f1dom3g  8907  xpdom3  9006  mapxpen  9074  dif1en  9089  findcard  9091  f1domfi2  9109  entrfir  9118  domtrfil  9119  domtrfir  9121  sbthfilem  9125  sdomdomtrfi  9128  php3  9136  findcard3  9186  indexfi  9263  suppr  9378  infpr  9411  r111  9690  tcrank  9799  acndom  9964  infdif2  10122  infxpdom  10123  cfeq0  10169  cfsuc  10170  cfflb  10172  cflim2  10176  cfsmolem  10183  axcc3  10351  domtriomlem  10355  axdc3lem2  10364  axdc3lem4  10366  axdc4lem  10368  axcclem  10370  pwcfsdom  10497  tsktrss  10675  tsksuc  10676  tskuni  10697  adderpqlem  10868  mulerpqlem  10869  mulcanenq  10874  distrnq  10875  ltsonq  10883  ltanq  10885  ltmnq  10886  distrlem1pr  10939  distrlem5pr  10941  ltsopr  10946  ltsosr  11008  ltasr  11014  adddir  11126  axlttrn  11209  letr  11231  nnncan1  11421  npncan3  11423  pnpcan2  11425  subdi  11574  subdir  11575  mulcan1g  11794  mulcan2g  11795  divmul  11803  div23  11819  div13  11821  muldivdir  11838  divsubdir  11839  subdivcomb1  11841  divcan7  11855  ltmul2  11997  lemul1  11998  lemul2  11999  lemul2a  12001  lediv1  12012  ltmuldiv2  12021  lemuldiv  12027  lemuldiv2  12028  ltdiv2  12033  lediv2  12037  infrelb  12132  nndivtr  12215  bndndx  12427  nn0n0n1ge2  12496  fnn0ind  12619  addlelt  13049  xrletr  13100  qsqueeze  13144  xleadd2a  13197  xleadd1  13198  xltadd2  13200  xltmul2  13236  supxrbnd  13271  iooneg  13415  iccneg  13416  icoshft  13417  icoshftf1o  13418  zltaddlt1le  13449  fzen  13486  uzsubsubfz  13491  ssfzunsnext  13514  fzrevral2  13558  fzshftral  13560  fz0fzdiffz0  13582  elfzmlbp  13584  elfzo  13606  nelfzo  13610  fzoaddel2  13666  fzosubel2  13671  ssfzo12bi  13707  fzonfzoufzol  13717  subfzo0  13738  flltdivnn0lt  13783  modmulnn  13839  modcyc  13856  modaddabs  13861  modaddmod  13862  modmuladd  13866  modadd2mod  13874  modsubmod  13882  modsubmodmod  13883  modaddmodup  13887  modmulmod  13889  modsubdir  13893  modfzo0difsn  13896  modsumfzodifsn  13897  uzindi  13935  axdc4uzlem  13936  expneg2  14023  expdiv  14066  expubnd  14131  mulbinom2  14176  bernneq2  14183  expnngt1  14194  hashinfxadd  14338  hashunsngx  14346  hashunsnggt  14347  hashfundm  14395  hashf1dmcdm  14397  hashdifsnp1  14459  ccatval3  14532  ccatfv0  14537  ccatval1lsw  14538  ccats1val2  14581  ccatw2s1p1  14590  swrdnd  14608  pfxsuffeqwrdeq  14651  pfxsuff1eqwrdeq  14652  swrdswrd  14658  pfxpfx  14661  wrd2ind  14676  swrdccatin1  14678  pfxccatin12lem1  14681  swrdccatin2  14682  pfxccatin12lem3  14685  swrdccat  14688  pfxccatpfx1  14689  pfxccatpfx2  14690  swrdccat3blem  14692  repswswrd  14737  repswpfx  14738  repswccat  14739  cshwidxmod  14756  2cshw  14766  3cshw  14771  scshwfzeqfzo  14779  cshwcsh2id  14781  cshimadifsn  14782  cshimadifsn0  14783  ccatco  14788  cshco  14789  swrdco  14790  pfxco  14791  lswco  14792  swrds2  14893  2swrd2eqwrdeq  14906  shftuz  15022  abs3dif  15285  fsumdifsnconst  15745  modfsummods  15747  sin02gt0  16150  dvdsval2  16215  dvdscmul  16242  dvdsmulc  16243  dvdscmulr  16244  dvdsmulcr  16245  divalglem8  16360  ndvdssub  16369  dvdsexpim  16515  rpmulgcd  16517  expgcd  16523  zexpgcd  16525  coprmprod  16621  cncongr1  16627  cncongr2  16628  isprm3  16643  modprm0  16767  coprimeprodsq  16770  pythagtriplem12  16788  pythagtriplem14  16790  pcprendvds  16802  pcmul  16813  pcdiv  16814  pcqcl  16818  pcqdiv  16819  pcdvdsb  16831  vdwnnlem1  16957  hashbcss  16966  cshwshashlem1  17057  fvsetsid  17129  setsstruct2  17135  setsstruct  17137  mrcss  17573  mrcsscl  17577  mrcun  17579  cofulid  17848  catcisolem  18068  funcsetcestrclem9  18120  latleeqj1  18408  lubun  18472  clatleglb  18475  pslem  18529  dirtr  18559  mgmb1mgm1  18614  pwspjmhm  18789  grpinvid1  18958  grpinvid2  18959  grpasscan1  18968  grpasscan2  18969  grpinvadd  18985  grpsubf  18986  grpsubrcan  18988  grpinvsub  18989  grpsubeq0  18993  grpsubadd0sub  18994  grppncan  18998  grpnpcan  18999  mulgnn0p1  19052  mulgaddcomlem  19064  mulginvcom  19066  mulginvinv  19067  subgsubcl  19104  subgsub  19105  eqglact  19145  qussub  19157  ghmsub  19190  psgnunilem4  19463  oddvds2  19532  odsubdvds  19537  gexnnod  19554  slwn0  19581  dvrcl  20375  unitdvcl  20376  dvrcan1  20380  dvrcan3  20381  dvreq1  20382  rngisom1  20437  rngisomring  20438  subrgdv  20557  abvsubtri  20795  idsrngd  20824  lmodvsubval2  20903  lsmcl  21070  lsmsp2  21074  lspsntrim  21085  rngqiprngimfolem  21280  lidldvgen  21324  cncrng  21378  chrcong  21517  dvdschrmulg  21518  zndvds  21539  zntoslem  21546  ocvsscon  21665  obselocv  21718  frlmphl  21771  ascldimul  21878  mpfsubrg  22099  ply1tmcl  22247  eqcoe1ply1eq  22274  gsummoncoe1  22283  lply1binomsc  22286  mamudm  22370  mamufacex  22371  scmatf1  22506  scmatf1o  22507  scmatrngiso  22511  submabas  22553  mdetdiaglem  22573  mdetralt2  22584  mdetero  22585  mdetunilem2  22588  mdetunilem6  22592  m2detleiblem7  22602  maducoeval2  22615  gsummatr01lem3  22632  gsummatr01  22634  smadiadetglem2  22647  cramerlem1  22662  mply1topmatcl  22780  mp2pm2mplem4  22784  ntrin  23036  elnei  23086  neindisj2  23098  ordtopn3  23171  leordtval2  23187  lecldbas  23194  cnrest2  23261  cmpsublem  23374  ptrescn  23614  xkococn  23635  kqfeq  23699  snfbas  23841  neifil  23855  fclsrest  23999  utopsnnei  24224  neipcfilu  24270  psmetsym  24285  psmetge0  24287  xmetge0  24319  xmetsym  24322  metustto  24528  metustbl  24541  restmetu  24545  nm2dif  24600  nmtri  24601  cnmet  24746  cnmpopc  24905  iihalf1  24908  iihalf2  24910  iocopnst  24917  clmnegsubdi2  25082  clmsub4  25083  clmvsubval2  25087  ncvspi  25133  cphsqrtcl3  25164  cph2ass  25190  cphipval2  25218  cphipval  25220  caublcls  25286  bcthlem3  25303  bcthlem4  25304  srabn  25337  cssbn  25352  cmslsschl  25354  rrxmet  25385  rrxdsfi  25388  iblconst  25795  dvdsq1p  26138  coeid3  26215  aannenlem2  26306  pserdvlem2  26406  tanord1  26514  cxpef  26642  recxpcl  26652  logbchbase  26748  relogbcl  26750  relogbzcl  26751  logbleb  26760  logblt  26761  relogbcxpb  26764  lawcos  26793  pythag  26794  isosctrlem1  26795  isosctrlem2  26796  lgsmodeq  27319  lgsmulsqcoprm  27320  gausslemma2dlem1a  27342  2lgsoddprmlem2  27386  ltsres  27640  lestr  27740  cofcutr  27930  lrrecpo  27947  ltadds2im  27992  leadds2im  27994  leadds1  27995  leadds2  27996  ltadds1  27998  addscan2  27999  addscan1  28000  ltsubs1  28082  divmulsw  28199  oldfib  28383  zsoring  28415  bdayfinbndlem1  28473  ax5seglem1  29011  axcontlem2  29048  axcontlem8  29054  upgrpredgv  29222  numedglnl  29227  issubgr2  29355  uhgrissubgr  29358  egrsubgr  29360  nbusgrfi  29457  nb3grprlem2  29464  cplgr3v  29518  cusgrsizeindslem  29535  finsumvtxdg2size  29634  rusgrpropadjvtx  29669  upgrwlkvtxedg  29728  usgr2trlncl  29843  uspgrn2crct  29891  crctcshwlkn0lem4  29896  crctcshwlkn0lem5  29897  wwlksnextproplem3  29994  umgr2adedgwlklem  30027  rusgr0edg  30059  clwwlk1loop  30073  clwwlkccatlem  30074  clwlkclwwlklem2a4  30082  clwlkclwwlklem2a  30083  clwwisshclwwslemlem  30098  erclwwlktr  30107  clwwlkel  30131  erclwwlkntr  30156  clwwlknonex2lem2  30193  uhgr3cyclex  30267  umgr3cyclex  30268  eucrctshift  30328  frgr3v  30360  3cyclfrgrrn  30371  frgrwopreglem5a  30396  frgr2wsp1  30415  extwwlkfab  30437  clwwlknonclwlknonf1o  30447  numclwwlk3lem1  30467  numclwwlk5  30473  numclwwlk6  30475  isgrpo  30583  grpoinvid1  30614  grpoinvid2  30615  grpoinvop  30619  grpodivinv  30622  grpoinvdiv  30623  grpodivf  30624  grponpcan  30629  ablonncan  30642  nvmval  30728  nvmval2  30729  nvmfval  30730  nvmul0or  30736  nvpncan2  30739  nvaddsub4  30743  nvmeq0  30744  nvdif  30752  nvpi  30753  nvmtri  30757  nvabs  30758  imsmetlem  30776  ipval2lem3  30791  ipval2  30793  4ipval2  30794  ipval3  30795  nmooge0  30853  blometi  30889  hvaddsub12  31124  hvsubdistr1  31135  hvsubdistr2  31136  hvaddcan2  31157  hvmulcan  31158  hvmulcan2  31159  hvsubcan  31160  hvsubcan2  31161  his7  31176  his2sub  31178  his2sub2  31179  norm3dif2  31237  shsubcl  31306  hhssnv  31350  shlej2  31447  fh2  31705  cm2j  31706  pjoi0  31803  hodcl  31833  hosubdi  31894  unopf1o  32002  unopadj  32005  adj2  32020  braadd  32031  bramul  32032  lnopaddmuli  32059  lnopsubmuli  32061  homco2  32063  lnfnaddmuli  32131  adjlnop  32172  leopmul  32220  leoptr  32223  pjimai  32262  atcv1  32466  atexch  32467  atcvatlem  32471  fcoinvbr  32690  preiman0  32798  divnumden2  32904  sgn3da  32922  xdivmul  32999  cshf1o  33037  resvsca  33407  idlsrgcmnd  33590  hasheuni  34245  difelsiga  34293  cndprobin  34594  bayesth  34599  signstfvp  34731  breprexplemc  34792  trssfir1om  35271  fineqvac  35276  fineqvnttrclselem1  35281  fineqvnttrclselem3  35283  trssfir1omregs  35296  swrdrevpfx  35315  swrdwlk  35325  lediv2aALT  35875  fununiq  35967  dfrdg2  35991  clsun  36526  neiin  36530  rdgeqoa  37700  curfv  37935  matunitlindflem1  37951  poimirlem32  37987  ftc1anclem4  38031  areacirc  38048  filbcmb  38075  ismtybnd  38142  grpoeqdivid  38216  ghomco  38226  rngonegrmul  38279  zerdivemp1x  38282  rngohomco  38309  rngoisoco  38317  riscer  38323  intidl  38364  isfldidl  38403  eceldmqsxrncnvepres  38771  eceldmqsxrncnvepres2  38772  brredunds  39045  lshpnelb  39444  opnlen0  39648  opcon3b  39656  opcon2b  39657  oplecon3b  39660  opltcon3b  39664  opltcon2b  39666  oldmm1  39677  oldmm4  39680  oldmj1  39681  oldmj4  39684  cvrval2  39734  cvrcon3b  39737  leatb  39752  atcmp  39771  atcvreq0  39774  atlatle  39780  athgt  39916  3dim2  39928  islln2a  39977  lplnnleat  40002  lvolnleat  40043  4atlem10  40066  4atlem11  40069  4atlem12  40072  dalem21  40154  dalem22  40155  dalem23  40156  dalem29  40161  dalem30  40162  dalem31N  40163  dalem32  40164  dalem33  40165  dalem34  40166  dalem35  40167  dalem36  40168  dalem37  40169  dalem40  40172  dalem46  40178  dalem47  40179  dalem51  40183  dalem52  40184  dalem58  40190  dalem59  40191  pmaple  40221  paddclN  40302  pmapjoin  40312  pmapjat1  40313  elpcliN  40353  pclssN  40354  pclun2N  40359  2polcon4bN  40378  paddunN  40387  poldmj1N  40388  pmapj2N  40389  pmapocjN  40390  psubclinN  40408  paddatclN  40409  poml4N  40413  lautco  40557  ldilco  40576  ltrneq2  40608  trljat1  40626  cdlemc1  40651  cdleme10  40714  ltrnco  41179  trlcocnv  41180  trljco  41200  trljco2  41201  cdlemi1  41278  tendocnv  41481  diaord  41507  dibord  41619  dihord3  41717  dihord4  41718  dihmeetlem2N  41759  dihmeetlem4preN  41766  dochdmj1  41850  hdmap10lem  42299  lcmineqlem1  42482  sticksstones2  42600  readdsub  42830  reltsub1  42832  renpncan3  42837  reppncan  42839  resubdi  42842  readdcan2  42859  mzprename  43195  dvdsrabdioph  43256  pell14qrdivcl  43311  monotoddzz  43389  jm2.19lem2  43436  jm2.19  43439  relexpaddss  44163  k0004lem3  44594  dvconstbi  44779  chordthmALT  45377  isosctrlem1ALT  45378  ssinc  45535  ssdec  45536  wessf1ornlem  45633  disjf1o  45639  ssnnf1octb  45642  projf1o  45644  mapssbi  45660  iunmapsn  45664  upbdrech  45756  iuneqfzuzlem  45782  suplesup  45787  rexabslelem  45864  climxrrelem  46195  limsupresxr  46212  liminfresxr  46213  liminfvalxr  46229  xlimliminflimsup  46308  cncfshift  46320  cncfperiod  46325  cncfuni  46332  icccncfext  46333  dvmptfprodlem  46390  dvnprodlem1  46392  itgspltprt  46425  ismbl3  46432  stoweidlem3  46449  stoweidlem10  46456  stoweidlem19  46465  stoweidlem31  46477  stoweidlem34  46480  stoweidlem44  46490  fourierdlem41  46594  fourierdlem42  46595  fourierdlem51  46603  fourierdlem68  46620  fourierdlem89  46641  fourierdlem91  46643  fourierdlem92  46644  fourierdlem94  46646  etransclem24  46704  etransclem34  46714  qndenserrnbllem  46740  salincl  46770  saldifcl2  46774  subsalsal  46805  sge0pr  46840  sge0pnffigt  46842  sge0reuz  46893  nnfoctbdjlem  46901  nnfoctbdj  46902  meadjiunlem  46911  caratheodorylem2  46973  hoidmv1le  47040  hoidmvlelem3  47043  hspmbllem2  47073  opnvonmbllem2  47079  sssmf  47184  smfaddlem1  47209  sigaraf  47299  sigarmf  47300  nltle2tri  47773  subsubelfzo0  47787  nnmul2  47790  submodaddmod  47807  zplusmodne  47809  addmodne  47810  minusmod5ne  47815  submodneaddmod  47817  modmkpkne  47827  modmknepk  47828  iccpartiltu  47894  icceuelpart  47908  poprelb  47996  reuopreuprim  47998  nprmmul2  48000  proththd  48089  mogoldbblem  48208  fppr2odd  48219  fpprel2  48229  bgoldbtbndlem2  48294  clnbusgrfi  48331  grimuhgr  48375  uhgrimisgrgric  48419  clnbgrgrim  48422  grtrif1o  48430  grlimgrtri  48491  gpgusgralem  48544  gpgedgvtx0  48549  gpgedg2ov  48554  gpgedg2iv  48555  gpg5nbgrvtx03starlem2  48557  nn0sumltlt  48838  invginvrid  48855  ply1sclrmsm  48872  linccl  48902  lincvalpr  48906  lincresunit3lem1  48967  lincresunit3  48969  fdivmpt  49028  nnolog2flm1  49078  dignnld  49091  digexp  49095  dignn0flhalflem1  49103  itcovalsucov  49156  reorelicc  49198  eenglngeehlnmlem1  49225  line2  49240  line2xlem  49241  itsclc0lem1  49244  itsclc0xyqsolr  49257  i0oii  49407  io1ii  49408  indthinc  49949  indthincALT  49950  setrec2fun  50179  reccot  50245  rectan  50246