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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  3ad2ant1  1134  3simpb  1150  3imp3i2an  1346  eupickb  2632  vtoclegftOLD  3573  eqeu  3700  onunel  6461  iotan0  6525  funopg  6574  fncoOLD  6658  dff1o2  6828  fvelimad  6948  unima  6955  fnimapr  6964  fvmptt  7007  fnreseql  7037  xpprsng  7125  f1elima  7249  f13dfv  7259  f1ocnvfvb  7264  f1cdmsn  7267  f1ofvswap  7291  oprssov  7563  funelss  8020  poxp  8101  poxp2  8116  poxp3  8123  wfrlem4OLD  8299  smoiso  8349  oaord  8535  oaword  8537  omcan  8557  omwordri  8560  odi  8567  omeulem1  8570  oeord  8576  oecan  8577  oewordri  8580  oeordsuc  8582  nnaord  8607  nnaordr  8608  nndi  8611  nnaword  8615  nnmwordri  8624  naddel2  8675  naddss1  8676  naddss2  8677  erov  8796  ecopovtrn  8802  mapsnd  8868  f1dom3g  8951  xpdom3  9058  mapxpen  9131  dif1en  9148  dif1enOLD  9150  findcard  9151  f1domfi2  9173  entrfir  9182  domtrfil  9183  domtrfir  9185  sbthfilem  9189  sdomdomtrfi  9192  php3  9200  findcard3  9273  indexfi  9348  suppr  9453  infpr  9485  r111  9757  tcrank  9866  acndom  10033  infdif2  10192  infxpdom  10193  cfeq0  10238  cfsuc  10239  cfflb  10241  cflim2  10245  cfsmolem  10252  axcc3  10420  domtriomlem  10424  axdc3lem2  10433  axdc3lem4  10435  axdc4lem  10437  axcclem  10439  pwcfsdom  10565  tsktrss  10743  tsksuc  10744  tskuni  10765  adderpqlem  10936  mulerpqlem  10937  mulcanenq  10942  distrnq  10943  ltsonq  10951  ltanq  10953  ltmnq  10954  distrlem1pr  11007  distrlem5pr  11009  ltsopr  11014  ltsosr  11076  ltasr  11082  adddir  11192  axlttrn  11273  letr  11295  nnncan1  11483  npncan3  11485  pnpcan2  11487  subdi  11634  subdir  11635  mulcan1g  11854  mulcan2g  11855  divmul  11862  div23  11878  div13  11880  muldivdir  11894  divsubdir  11895  subdivcomb1  11896  divcan7  11910  ltmul2  12052  lemul1  12053  lemul2  12054  lemul2a  12056  lediv1  12066  ltmuldiv2  12075  lemuldiv  12081  lemuldiv2  12082  ltdiv2  12087  lediv2  12091  infrelb  12186  nndivtr  12246  bndndx  12458  nn0n0n1ge2  12526  fnn0ind  12648  addlelt  13075  xrletr  13124  qsqueeze  13167  xleadd2a  13220  xleadd1  13221  xltadd2  13223  xltmul2  13259  supxrbnd  13294  iooneg  13435  iccneg  13436  icoshft  13437  icoshftf1o  13438  zltaddlt1le  13469  fzen  13505  uzsubsubfz  13510  ssfzunsnext  13533  fzrevral2  13574  fzshftral  13576  fz0fzdiffz0  13597  elfzmlbp  13599  elfzo  13621  nelfzo  13624  fzoaddel2  13675  fzosubel2  13679  ssfzo12bi  13714  fzonfzoufzol  13722  subfzo0  13741  flltdivnn0lt  13785  modmulnn  13841  modcyc  13858  modaddabs  13861  modaddmod  13862  modmuladd  13865  modadd2mod  13873  modsubmod  13881  modsubmodmod  13882  modaddmodup  13886  modmulmod  13888  modsubdir  13892  modfzo0difsn  13895  modsumfzodifsn  13896  uzindi  13934  axdc4uzlem  13935  expneg2  14023  expdiv  14066  expubnd  14129  mulbinom2  14173  bernneq2  14180  expnngt1  14191  hashinfxadd  14332  hashunsngx  14340  hashunsnggt  14341  hashfundm  14389  hashdifsnp1  14444  ccatval3  14516  ccatfv0  14520  ccatval1lsw  14521  ccats1val2  14564  ccatw2s1p1  14573  swrdnd  14591  pfxsuffeqwrdeq  14635  pfxsuff1eqwrdeq  14636  swrdswrd  14642  pfxpfx  14645  wrd2ind  14660  swrdccatin1  14662  pfxccatin12lem1  14665  swrdccatin2  14666  pfxccatin12lem3  14669  swrdccat  14672  pfxccatpfx1  14673  pfxccatpfx2  14674  swrdccat3blem  14676  repswswrd  14721  repswpfx  14722  repswccat  14723  cshwidxmod  14740  2cshw  14750  3cshw  14755  scshwfzeqfzo  14764  cshwcsh2id  14766  cshimadifsn  14767  cshimadifsn0  14768  ccatco  14773  cshco  14774  swrdco  14775  pfxco  14776  lswco  14777  swrds2  14878  2swrd2eqwrdeq  14891  shftuz  15003  abs3dif  15265  fsumdifsnconst  15724  modfsummods  15726  sin02gt0  16122  dvdsval2  16187  dvdscmul  16213  dvdsmulc  16214  dvdscmulr  16215  dvdsmulcr  16216  divalglem8  16330  ndvdssub  16339  rpmulgcd  16485  coprmprod  16585  cncongr1  16591  cncongr2  16592  isprm3  16607  modprm0  16725  coprimeprodsq  16728  pythagtriplem12  16746  pythagtriplem14  16748  pcprendvds  16760  pcmul  16771  pcdiv  16772  pcqcl  16776  pcqdiv  16777  pcdvdsb  16789  vdwnnlem1  16915  hashbcss  16924  cshwshashlem1  17016  fvsetsid  17088  setsstruct2  17094  setsstruct  17096  mrcss  17547  mrcsscl  17551  mrcun  17553  cofulid  17827  catcisolem  18047  funcsetcestrclem9  18102  latleeqj1  18391  lubun  18455  clatleglb  18458  pslem  18512  dirtr  18542  mgmb1mgm1  18561  pwspjmhm  18698  grpinvid1  18863  grpinvid2  18864  grpasscan1  18873  grpasscan2  18874  grpinvadd  18888  grpsubf  18889  grpsubrcan  18891  grpinvsub  18892  grpsubeq0  18896  grpsubadd0sub  18897  grppncan  18901  grpnpcan  18902  mulgnn0p1  18950  mulgaddcomlem  18962  mulginvcom  18964  mulginvinv  18965  subgsubcl  19002  subgsub  19003  eqglact  19044  qussub  19055  ghmsub  19085  psgnunilem4  19349  oddvds2  19418  odsubdvds  19423  gexnnod  19440  slwn0  19467  dvrcl  20196  unitdvcl  20197  dvrcan1  20201  dvrcan3  20202  dvreq1  20203  subrgdv  20357  abvsubtri  20420  idsrngd  20447  lmodvsubval2  20504  lsmcl  20671  lsmsp2  20675  lspsntrim  20686  lidldvgen  20869  chrcong  21054  zndvds  21078  zntoslem  21085  ocvsscon  21201  obselocv  21256  frlmphl  21309  ascldimul  21413  mpfsubrg  21635  ply1tmcl  21765  eqcoe1ply1eq  21790  gsummoncoe1  21797  lply1binomsc  21800  mamudm  21859  mamufacex  21860  scmatf1  22002  scmatf1o  22003  scmatrngiso  22007  submabas  22049  mdetdiaglem  22069  mdetralt2  22080  mdetero  22081  mdetunilem2  22084  mdetunilem6  22088  m2detleiblem7  22098  maducoeval2  22111  gsummatr01lem3  22128  gsummatr01  22130  smadiadetglem2  22143  cramerlem1  22158  mply1topmatcl  22276  mp2pm2mplem4  22280  ntrin  22534  elnei  22584  neindisj2  22596  ordtopn3  22669  leordtval2  22685  lecldbas  22692  cnrest2  22759  cmpsublem  22872  ptrescn  23112  xkococn  23133  kqfeq  23197  snfbas  23339  neifil  23353  fclsrest  23497  utopsnnei  23723  neipcfilu  23770  psmetsym  23785  psmetge0  23787  xmetge0  23819  xmetsym  23822  metustto  24031  metustbl  24044  restmetu  24048  nm2dif  24103  nmtri  24104  cnmet  24257  cnmpopc  24413  iihalf1  24416  iihalf2  24418  iocopnst  24425  clmnegsubdi2  24590  clmsub4  24591  clmvsubval2  24595  ncvspi  24642  cphsqrtcl3  24673  cph2ass  24699  cphipval2  24727  cphipval  24729  caublcls  24795  bcthlem3  24812  bcthlem4  24813  srabn  24846  cssbn  24861  cmslsschl  24863  rrxmet  24894  rrxdsfi  24897  iblconst  25304  tdeglem3OLD  25545  dvdsq1p  25647  coeid3  25723  aannenlem2  25811  pserdvlem2  25909  tanord1  26015  cxpef  26142  recxpcl  26152  logbchbase  26243  relogbcl  26245  relogbzcl  26246  logbleb  26255  logblt  26256  relogbcxpb  26259  lawcos  26288  pythag  26289  isosctrlem1  26290  isosctrlem2  26291  lgsmodeq  26812  lgsmulsqcoprm  26813  gausslemma2dlem1a  26835  2lgsoddprmlem2  26879  sltres  27132  sletr  27228  cofcutr  27378  lrrecpo  27392  sltadd2im  27436  sleadd2im  27438  sleadd1  27439  sleadd2  27440  sltadd1  27442  addscan2  27443  addscan1  27444  sltsub1  27510  divsmulw  27607  ax5seglem1  28153  axcontlem2  28190  axcontlem8  28196  upgrpredgv  28366  numedglnl  28371  issubgr2  28496  uhgrissubgr  28499  egrsubgr  28501  nbusgrfi  28598  nb3grprlem2  28605  cplgr3v  28659  cusgrsizeindslem  28675  finsumvtxdg2size  28774  rusgrpropadjvtx  28809  upgrwlkvtxedg  28869  usgr2trlncl  28984  uspgrn2crct  29029  crctcshwlkn0lem4  29034  crctcshwlkn0lem5  29035  wwlksnextproplem3  29132  umgr2adedgwlklem  29165  rusgr0edg  29194  clwwlk1loop  29208  clwwlkccatlem  29209  clwlkclwwlklem2a4  29217  clwlkclwwlklem2a  29218  clwwisshclwwslemlem  29233  erclwwlktr  29242  clwwlkel  29266  erclwwlkntr  29291  clwwlknonex2lem2  29328  uhgr3cyclex  29402  umgr3cyclex  29403  eucrctshift  29463  frgr3v  29495  3cyclfrgrrn  29506  frgrwopreglem5a  29531  frgr2wsp1  29550  extwwlkfab  29572  clwwlknonclwlknonf1o  29582  numclwwlk3lem1  29602  numclwwlk5  29608  numclwwlk6  29610  isgrpo  29715  grpoinvid1  29746  grpoinvid2  29747  grpoinvop  29751  grpodivinv  29754  grpoinvdiv  29755  grpodivf  29756  grponpcan  29761  ablonncan  29774  nvmval  29860  nvmval2  29861  nvmfval  29862  nvmul0or  29868  nvpncan2  29871  nvaddsub4  29875  nvmeq0  29876  nvdif  29884  nvpi  29885  nvmtri  29889  nvabs  29890  imsmetlem  29908  ipval2lem3  29923  ipval2  29925  4ipval2  29926  ipval3  29927  nmooge0  29985  blometi  30021  hvaddsub12  30256  hvsubdistr1  30267  hvsubdistr2  30268  hvaddcan2  30289  hvmulcan  30290  hvmulcan2  30291  hvsubcan  30292  hvsubcan2  30293  his7  30308  his2sub  30310  his2sub2  30311  norm3dif2  30369  shsubcl  30438  hhssnv  30482  shlej2  30579  fh2  30837  cm2j  30838  pjoi0  30935  hodcl  30965  hosubdi  31026  unopf1o  31134  unopadj  31137  adj2  31152  braadd  31163  bramul  31164  lnopaddmuli  31191  lnopsubmuli  31193  homco2  31195  lnfnaddmuli  31263  adjlnop  31304  leopmul  31352  leoptr  31355  pjimai  31394  atcv1  31598  atexch  31599  atcvatlem  31603  fcoinvbr  31805  preiman0  31902  divnumden2  31995  xdivmul  32062  cshf1o  32097  dvdschrmulg  32348  resvsca  32406  idlsrgcmnd  32574  hasheuni  33014  difelsiga  33062  cndprobin  33364  bayesth  33369  sgn3da  33471  signstfvp  33513  breprexplemc  33575  fineqvac  34028  hashf1dmcdm  34036  swrdrevpfx  34038  swrdwlk  34048  lediv2aALT  34593  fununiq  34671  dfrdg2  34698  clsun  35118  neiin  35122  rdgeqoa  36156  curfv  36373  matunitlindflem1  36389  poimirlem32  36425  ftc1anclem4  36469  areacirc  36486  filbcmb  36514  ismtybnd  36581  grpoeqdivid  36655  ghomco  36665  rngonegrmul  36718  zerdivemp1x  36721  rngohomco  36748  rngoisoco  36756  riscer  36762  intidl  36803  isfldidl  36842  brredunds  37402  lshpnelb  37760  opnlen0  37964  opcon3b  37972  opcon2b  37973  oplecon3b  37976  opltcon3b  37980  opltcon2b  37982  oldmm1  37993  oldmm4  37996  oldmj1  37997  oldmj4  38000  cvrval2  38050  cvrcon3b  38053  leatb  38068  atcmp  38087  atcvreq0  38090  atlatle  38096  athgt  38233  3dim2  38245  islln2a  38294  lplnnleat  38319  lvolnleat  38360  4atlem10  38383  4atlem11  38386  4atlem12  38389  dalem21  38471  dalem22  38472  dalem23  38473  dalem29  38478  dalem30  38479  dalem31N  38480  dalem32  38481  dalem33  38482  dalem34  38483  dalem35  38484  dalem36  38485  dalem37  38486  dalem40  38489  dalem46  38495  dalem47  38496  dalem51  38500  dalem52  38501  dalem58  38507  dalem59  38508  pmaple  38538  paddclN  38619  pmapjoin  38629  pmapjat1  38630  elpcliN  38670  pclssN  38671  pclun2N  38676  2polcon4bN  38695  paddunN  38704  poldmj1N  38705  pmapj2N  38706  pmapocjN  38707  psubclinN  38725  paddatclN  38726  poml4N  38730  lautco  38874  ldilco  38893  ltrneq2  38925  trljat1  38943  cdlemc1  38968  cdleme10  39031  ltrnco  39496  trlcocnv  39497  trljco  39517  trljco2  39518  cdlemi1  39595  tendocnv  39798  diaord  39824  dibord  39936  dihord3  40034  dihord4  40035  dihmeetlem2N  40076  dihmeetlem4preN  40083  dochdmj1  40167  hdmap10lem  40616  lcmineqlem1  40800  sticksstones2  40869  metakunt29  40919  metakunt30  40920  factwoffsmonot  40929  dvdsexpim  41100  expgcd  41106  zexpgcd  41108  readdsub  41139  reltsub1  41141  renpncan3  41146  reppncan  41148  resubdi  41151  readdcan2  41167  mzprename  41358  dvdsrabdioph  41419  pell14qrdivcl  41474  monotoddzz  41553  jm2.19lem2  41600  jm2.19  41603  relexpaddss  42340  k0004lem3  42771  dvconstbi  42964  chordthmALT  43565  isosctrlem1ALT  43566  ssinc  43647  ssdec  43648  wessf1ornlem  43753  disjf1o  43760  ssnnf1octb  43764  projf1o  43767  mapssbi  43783  iunmapsn  43787  upbdrech  43888  iuneqfzuzlem  43917  suplesup  43922  rexabslelem  44001  climxrrelem  44338  limsupresxr  44355  liminfresxr  44356  liminfvalxr  44372  xlimliminflimsup  44451  cncfshift  44463  cncfperiod  44468  cncfuni  44475  icccncfext  44476  dvmptfprodlem  44533  dvnprodlem1  44535  itgspltprt  44568  ismbl3  44575  stoweidlem3  44592  stoweidlem10  44599  stoweidlem19  44608  stoweidlem31  44620  stoweidlem34  44623  stoweidlem44  44633  fourierdlem41  44737  fourierdlem42  44738  fourierdlem51  44746  fourierdlem68  44763  fourierdlem89  44784  fourierdlem91  44786  fourierdlem92  44787  fourierdlem94  44789  etransclem24  44847  etransclem34  44857  qndenserrnbllem  44883  salincl  44913  saldifcl2  44917  subsalsal  44948  sge0pr  44983  sge0pnffigt  44985  sge0reuz  45036  nnfoctbdjlem  45044  nnfoctbdj  45045  meadjiunlem  45054  caratheodorylem2  45116  hoidmv1le  45183  hoidmvlelem3  45186  hspmbllem2  45216  opnvonmbllem2  45222  sssmf  45327  smfaddlem1  45352  sigaraf  45442  sigarmf  45443  nltle2tri  45894  subsubelfzo0  45907  iccpartiltu  45963  icceuelpart  45977  poprelb  46065  reuopreuprim  46067  proththd  46155  mogoldbblem  46261  fppr2odd  46272  fpprel2  46282  bgoldbtbndlem2  46347  isomgrtr  46380  rngisom1  46590  rngisomring  46591  rngqiprngimfolem  46642  nn0sumltlt  46866  invginvrid  46883  ply1sclrmsm  46904  linccl  46935  lincvalpr  46939  lincresunit3lem1  47000  lincresunit3  47002  fdivmpt  47066  nnolog2flm1  47116  dignnld  47129  digexp  47133  dignn0flhalflem1  47141  itcovalsucov  47194  reorelicc  47236  eenglngeehlnmlem1  47263  line2  47278  line2xlem  47279  itsclc0lem1  47282  itsclc0xyqsolr  47295  i0oii  47392  io1ii  47393  indthinc  47512  indthincALT  47513  setrec2fun  47577  reccot  47643  rectan  47644