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 714	. 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  1133  3simpb  1149  3imp3i2an  1345  eupickb  2638  vtoclegftOLD  3602  eqeu  3728  onunel  6500  iotan0  6563  funopg  6612  fncoOLD  6698  dff1o2  6867  fvelimad  6989  unima  6997  fnimapr  7005  fvmptt  7049  fnreseql  7081  xpprsng  7174  f1elima  7300  f13dfv  7310  f1ocnvfvb  7315  f1cdmsn  7318  f1ofvswap  7342  oprssov  7619  funelss  8088  poxp  8169  poxp2  8184  poxp3  8191  wfrlem4OLD  8368  smoiso  8418  oaord  8603  oaword  8605  omcan  8625  omwordri  8628  odi  8635  omeulem1  8638  oeord  8644  oecan  8645  oewordri  8648  oeordsuc  8650  nnaord  8675  nnaordr  8676  nndi  8679  nnaword  8683  nnmwordri  8692  naddel2  8744  naddss1  8745  naddss2  8746  erov  8872  ecopovtrn  8878  mapsnd  8944  f1dom3g  9027  xpdom3  9136  mapxpen  9209  dif1en  9226  dif1enOLD  9228  findcard  9229  f1domfi2  9248  entrfir  9257  domtrfil  9258  domtrfir  9260  sbthfilem  9264  sdomdomtrfi  9267  php3  9275  findcard3  9346  indexfi  9430  suppr  9540  infpr  9572  r111  9844  tcrank  9953  acndom  10120  infdif2  10278  infxpdom  10279  cfeq0  10325  cfsuc  10326  cfflb  10328  cflim2  10332  cfsmolem  10339  axcc3  10507  domtriomlem  10511  axdc3lem2  10520  axdc3lem4  10522  axdc4lem  10524  axcclem  10526  pwcfsdom  10652  tsktrss  10830  tsksuc  10831  tskuni  10852  adderpqlem  11023  mulerpqlem  11024  mulcanenq  11029  distrnq  11030  ltsonq  11038  ltanq  11040  ltmnq  11041  distrlem1pr  11094  distrlem5pr  11096  ltsopr  11101  ltsosr  11163  ltasr  11169  adddir  11281  axlttrn  11362  letr  11384  nnncan1  11572  npncan3  11574  pnpcan2  11576  subdi  11723  subdir  11724  mulcan1g  11943  mulcan2g  11944  divmul  11952  div23  11968  div13  11970  muldivdir  11987  divsubdir  11988  subdivcomb1  11989  divcan7  12003  ltmul2  12145  lemul1  12146  lemul2  12147  lemul2a  12149  lediv1  12160  ltmuldiv2  12169  lemuldiv  12175  lemuldiv2  12176  ltdiv2  12181  lediv2  12185  infrelb  12280  nndivtr  12340  bndndx  12552  nn0n0n1ge2  12620  fnn0ind  12742  addlelt  13171  xrletr  13220  qsqueeze  13263  xleadd2a  13316  xleadd1  13317  xltadd2  13319  xltmul2  13355  supxrbnd  13390  iooneg  13531  iccneg  13532  icoshft  13533  icoshftf1o  13534  zltaddlt1le  13565  fzen  13601  uzsubsubfz  13606  ssfzunsnext  13629  fzrevral2  13670  fzshftral  13672  fz0fzdiffz0  13694  elfzmlbp  13696  elfzo  13718  nelfzo  13721  fzoaddel2  13772  fzosubel2  13776  ssfzo12bi  13811  fzonfzoufzol  13820  subfzo0  13839  flltdivnn0lt  13884  modmulnn  13940  modcyc  13957  modaddabs  13960  modaddmod  13961  modmuladd  13964  modadd2mod  13972  modsubmod  13980  modsubmodmod  13981  modaddmodup  13985  modmulmod  13987  modsubdir  13991  modfzo0difsn  13994  modsumfzodifsn  13995  uzindi  14033  axdc4uzlem  14034  expneg2  14121  expdiv  14164  expubnd  14227  mulbinom2  14272  bernneq2  14279  expnngt1  14290  hashinfxadd  14434  hashunsngx  14442  hashunsnggt  14443  hashfundm  14491  hashf1dmcdm  14493  hashdifsnp1  14555  ccatval3  14627  ccatfv0  14631  ccatval1lsw  14632  ccats1val2  14675  ccatw2s1p1  14684  swrdnd  14702  pfxsuffeqwrdeq  14746  pfxsuff1eqwrdeq  14747  swrdswrd  14753  pfxpfx  14756  wrd2ind  14771  swrdccatin1  14773  pfxccatin12lem1  14776  swrdccatin2  14777  pfxccatin12lem3  14780  swrdccat  14783  pfxccatpfx1  14784  pfxccatpfx2  14785  swrdccat3blem  14787  repswswrd  14832  repswpfx  14833  repswccat  14834  cshwidxmod  14851  2cshw  14861  3cshw  14866  scshwfzeqfzo  14875  cshwcsh2id  14877  cshimadifsn  14878  cshimadifsn0  14879  ccatco  14884  cshco  14885  swrdco  14886  pfxco  14887  lswco  14888  swrds2  14989  2swrd2eqwrdeq  15002  shftuz  15118  abs3dif  15380  fsumdifsnconst  15839  modfsummods  15841  sin02gt0  16240  dvdsval2  16305  dvdscmul  16331  dvdsmulc  16332  dvdscmulr  16333  dvdsmulcr  16334  divalglem8  16448  ndvdssub  16457  dvdsexpim  16602  rpmulgcd  16604  expgcd  16610  zexpgcd  16612  coprmprod  16708  cncongr1  16714  cncongr2  16715  isprm3  16730  modprm0  16852  coprimeprodsq  16855  pythagtriplem12  16873  pythagtriplem14  16875  pcprendvds  16887  pcmul  16898  pcdiv  16899  pcqcl  16903  pcqdiv  16904  pcdvdsb  16916  vdwnnlem1  17042  hashbcss  17051  cshwshashlem1  17143  fvsetsid  17215  setsstruct2  17221  setsstruct  17223  mrcss  17674  mrcsscl  17678  mrcun  17680  cofulid  17954  catcisolem  18177  funcsetcestrclem9  18232  latleeqj1  18521  lubun  18585  clatleglb  18588  pslem  18642  dirtr  18672  mgmb1mgm1  18693  pwspjmhm  18865  grpinvid1  19031  grpinvid2  19032  grpasscan1  19041  grpasscan2  19042  grpinvadd  19058  grpsubf  19059  grpsubrcan  19061  grpinvsub  19062  grpsubeq0  19066  grpsubadd0sub  19067  grppncan  19071  grpnpcan  19072  mulgnn0p1  19125  mulgaddcomlem  19137  mulginvcom  19139  mulginvinv  19140  subgsubcl  19177  subgsub  19178  eqglact  19219  qussub  19231  ghmsub  19264  psgnunilem4  19539  oddvds2  19608  odsubdvds  19613  gexnnod  19630  slwn0  19657  dvrcl  20430  unitdvcl  20431  dvrcan1  20435  dvrcan3  20436  dvreq1  20437  rngisom1  20492  rngisomring  20493  subrgdv  20617  abvsubtri  20850  idsrngd  20879  lmodvsubval2  20937  lsmcl  21105  lsmsp2  21109  lspsntrim  21120  rngqiprngimfolem  21323  lidldvgen  21367  cncrng  21424  chrcong  21565  dvdschrmulg  21566  zndvds  21591  zntoslem  21598  ocvsscon  21716  obselocv  21771  frlmphl  21824  ascldimul  21931  mpfsubrg  22150  ply1tmcl  22296  eqcoe1ply1eq  22324  gsummoncoe1  22333  lply1binomsc  22336  mamudm  22420  mamufacex  22421  scmatf1  22558  scmatf1o  22559  scmatrngiso  22563  submabas  22605  mdetdiaglem  22625  mdetralt2  22636  mdetero  22637  mdetunilem2  22640  mdetunilem6  22644  m2detleiblem7  22654  maducoeval2  22667  gsummatr01lem3  22684  gsummatr01  22686  smadiadetglem2  22699  cramerlem1  22714  mply1topmatcl  22832  mp2pm2mplem4  22836  ntrin  23090  elnei  23140  neindisj2  23152  ordtopn3  23225  leordtval2  23241  lecldbas  23248  cnrest2  23315  cmpsublem  23428  ptrescn  23668  xkococn  23689  kqfeq  23753  snfbas  23895  neifil  23909  fclsrest  24053  utopsnnei  24279  neipcfilu  24326  psmetsym  24341  psmetge0  24343  xmetge0  24375  xmetsym  24378  metustto  24587  metustbl  24600  restmetu  24604  nm2dif  24659  nmtri  24660  cnmet  24813  cnmpopc  24974  iihalf1  24977  iihalf2  24980  iocopnst  24989  clmnegsubdi2  25157  clmsub4  25158  clmvsubval2  25162  ncvspi  25209  cphsqrtcl3  25240  cph2ass  25266  cphipval2  25294  cphipval  25296  caublcls  25362  bcthlem3  25379  bcthlem4  25380  srabn  25413  cssbn  25428  cmslsschl  25430  rrxmet  25461  rrxdsfi  25464  iblconst  25873  dvdsq1p  26222  coeid3  26299  aannenlem2  26389  pserdvlem2  26490  tanord1  26597  cxpef  26725  recxpcl  26735  logbchbase  26832  relogbcl  26834  relogbzcl  26835  logbleb  26844  logblt  26845  relogbcxpb  26848  lawcos  26877  pythag  26878  isosctrlem1  26879  isosctrlem2  26880  lgsmodeq  27404  lgsmulsqcoprm  27405  gausslemma2dlem1a  27427  2lgsoddprmlem2  27471  sltres  27725  sletr  27821  cofcutr  27976  lrrecpo  27992  sltadd2im  28037  sleadd2im  28039  sleadd1  28040  sleadd2  28041  sltadd1  28043  addscan2  28044  addscan1  28045  sltsub1  28124  divsmulw  28236  ax5seglem1  28961  axcontlem2  28998  axcontlem8  29004  upgrpredgv  29174  numedglnl  29179  issubgr2  29307  uhgrissubgr  29310  egrsubgr  29312  nbusgrfi  29409  nb3grprlem2  29416  cplgr3v  29470  cusgrsizeindslem  29487  finsumvtxdg2size  29586  rusgrpropadjvtx  29621  upgrwlkvtxedg  29681  usgr2trlncl  29796  uspgrn2crct  29841  crctcshwlkn0lem4  29846  crctcshwlkn0lem5  29847  wwlksnextproplem3  29944  umgr2adedgwlklem  29977  rusgr0edg  30006  clwwlk1loop  30020  clwwlkccatlem  30021  clwlkclwwlklem2a4  30029  clwlkclwwlklem2a  30030  clwwisshclwwslemlem  30045  erclwwlktr  30054  clwwlkel  30078  erclwwlkntr  30103  clwwlknonex2lem2  30140  uhgr3cyclex  30214  umgr3cyclex  30215  eucrctshift  30275  frgr3v  30307  3cyclfrgrrn  30318  frgrwopreglem5a  30343  frgr2wsp1  30362  extwwlkfab  30384  clwwlknonclwlknonf1o  30394  numclwwlk3lem1  30414  numclwwlk5  30420  numclwwlk6  30422  isgrpo  30529  grpoinvid1  30560  grpoinvid2  30561  grpoinvop  30565  grpodivinv  30568  grpoinvdiv  30569  grpodivf  30570  grponpcan  30575  ablonncan  30588  nvmval  30674  nvmval2  30675  nvmfval  30676  nvmul0or  30682  nvpncan2  30685  nvaddsub4  30689  nvmeq0  30690  nvdif  30698  nvpi  30699  nvmtri  30703  nvabs  30704  imsmetlem  30722  ipval2lem3  30737  ipval2  30739  4ipval2  30740  ipval3  30741  nmooge0  30799  blometi  30835  hvaddsub12  31070  hvsubdistr1  31081  hvsubdistr2  31082  hvaddcan2  31103  hvmulcan  31104  hvmulcan2  31105  hvsubcan  31106  hvsubcan2  31107  his7  31122  his2sub  31124  his2sub2  31125  norm3dif2  31183  shsubcl  31252  hhssnv  31296  shlej2  31393  fh2  31651  cm2j  31652  pjoi0  31749  hodcl  31779  hosubdi  31840  unopf1o  31948  unopadj  31951  adj2  31966  braadd  31977  bramul  31978  lnopaddmuli  32005  lnopsubmuli  32007  homco2  32009  lnfnaddmuli  32077  adjlnop  32118  leopmul  32166  leoptr  32169  pjimai  32208  atcv1  32412  atexch  32413  atcvatlem  32417  fcoinvbr  32627  preiman0  32721  divnumden2  32819  xdivmul  32889  cshf1o  32929  resvsca  33321  idlsrgcmnd  33508  hasheuni  34049  difelsiga  34097  cndprobin  34399  bayesth  34404  sgn3da  34506  signstfvp  34548  breprexplemc  34609  fineqvac  35073  swrdrevpfx  35084  swrdwlk  35094  lediv2aALT  35645  fununiq  35732  dfrdg2  35759  clsun  36294  neiin  36298  rdgeqoa  37336  curfv  37560  matunitlindflem1  37576  poimirlem32  37612  ftc1anclem4  37656  areacirc  37673  filbcmb  37700  ismtybnd  37767  grpoeqdivid  37841  ghomco  37851  rngonegrmul  37904  zerdivemp1x  37907  rngohomco  37934  rngoisoco  37942  riscer  37948  intidl  37989  isfldidl  38028  brredunds  38582  lshpnelb  38940  opnlen0  39144  opcon3b  39152  opcon2b  39153  oplecon3b  39156  opltcon3b  39160  opltcon2b  39162  oldmm1  39173  oldmm4  39176  oldmj1  39177  oldmj4  39180  cvrval2  39230  cvrcon3b  39233  leatb  39248  atcmp  39267  atcvreq0  39270  atlatle  39276  athgt  39413  3dim2  39425  islln2a  39474  lplnnleat  39499  lvolnleat  39540  4atlem10  39563  4atlem11  39566  4atlem12  39569  dalem21  39651  dalem22  39652  dalem23  39653  dalem29  39658  dalem30  39659  dalem31N  39660  dalem32  39661  dalem33  39662  dalem34  39663  dalem35  39664  dalem36  39665  dalem37  39666  dalem40  39669  dalem46  39675  dalem47  39676  dalem51  39680  dalem52  39681  dalem58  39687  dalem59  39688  pmaple  39718  paddclN  39799  pmapjoin  39809  pmapjat1  39810  elpcliN  39850  pclssN  39851  pclun2N  39856  2polcon4bN  39875  paddunN  39884  poldmj1N  39885  pmapj2N  39886  pmapocjN  39887  psubclinN  39905  paddatclN  39906  poml4N  39910  lautco  40054  ldilco  40073  ltrneq2  40105  trljat1  40123  cdlemc1  40148  cdleme10  40211  ltrnco  40676  trlcocnv  40677  trljco  40697  trljco2  40698  cdlemi1  40775  tendocnv  40978  diaord  41004  dibord  41116  dihord3  41214  dihord4  41215  dihmeetlem2N  41256  dihmeetlem4preN  41263  dochdmj1  41347  hdmap10lem  41796  lcmineqlem1  41986  sticksstones2  42104  metakunt29  42190  metakunt30  42191  factwoffsmonot  42199  readdsub  42360  reltsub1  42362  renpncan3  42367  reppncan  42369  resubdi  42372  readdcan2  42388  mzprename  42705  dvdsrabdioph  42766  pell14qrdivcl  42821  monotoddzz  42900  jm2.19lem2  42947  jm2.19  42950  relexpaddss  43680  k0004lem3  44111  dvconstbi  44303  chordthmALT  44904  isosctrlem1ALT  44905  ssinc  44989  ssdec  44990  wessf1ornlem  45092  disjf1o  45098  ssnnf1octb  45101  projf1o  45104  mapssbi  45120  iunmapsn  45124  upbdrech  45220  iuneqfzuzlem  45249  suplesup  45254  rexabslelem  45333  climxrrelem  45670  limsupresxr  45687  liminfresxr  45688  liminfvalxr  45704  xlimliminflimsup  45783  cncfshift  45795  cncfperiod  45800  cncfuni  45807  icccncfext  45808  dvmptfprodlem  45865  dvnprodlem1  45867  itgspltprt  45900  ismbl3  45907  stoweidlem3  45924  stoweidlem10  45931  stoweidlem19  45940  stoweidlem31  45952  stoweidlem34  45955  stoweidlem44  45965  fourierdlem41  46069  fourierdlem42  46070  fourierdlem51  46078  fourierdlem68  46095  fourierdlem89  46116  fourierdlem91  46118  fourierdlem92  46119  fourierdlem94  46121  etransclem24  46179  etransclem34  46189  qndenserrnbllem  46215  salincl  46245  saldifcl2  46249  subsalsal  46280  sge0pr  46315  sge0pnffigt  46317  sge0reuz  46368  nnfoctbdjlem  46376  nnfoctbdj  46377  meadjiunlem  46386  caratheodorylem2  46448  hoidmv1le  46515  hoidmvlelem3  46518  hspmbllem2  46548  opnvonmbllem2  46554  sssmf  46659  smfaddlem1  46684  sigaraf  46774  sigarmf  46775  nltle2tri  47228  subsubelfzo0  47241  iccpartiltu  47296  icceuelpart  47310  poprelb  47398  reuopreuprim  47400  proththd  47488  mogoldbblem  47594  fppr2odd  47605  fpprel2  47615  bgoldbtbndlem2  47680  clnbusgrfi  47715  grimuhgr  47762  uhgrimisgrgric  47783  clnbgrgrim  47786  grtrif1o  47793  grlimgrtri  47820  nn0sumltlt  48075  invginvrid  48092  ply1sclrmsm  48112  linccl  48143  lincvalpr  48147  lincresunit3lem1  48208  lincresunit3  48210  fdivmpt  48274  nnolog2flm1  48324  dignnld  48337  digexp  48341  dignn0flhalflem1  48349  itcovalsucov  48402  reorelicc  48444  eenglngeehlnmlem1  48471  line2  48486  line2xlem  48487  itsclc0lem1  48490  itsclc0xyqsolr  48503  i0oii  48599  io1ii  48600  indthinc  48719  indthincALT  48720  setrec2fun  48784  reccot  48850  rectan  48851