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  3575  eqeu  3702  onunel  6467  iotan0  6531  funopg  6580  fncoOLD  6666  dff1o2  6836  fvelimad  6957  unima  6964  fnimapr  6973  fvmptt  7016  fnreseql  7047  xpprsng  7135  f1elima  7259  f13dfv  7269  f1ocnvfvb  7274  f1cdmsn  7277  f1ofvswap  7301  oprssov  7573  funelss  8030  poxp  8111  poxp2  8126  poxp3  8133  wfrlem4OLD  8309  smoiso  8359  oaord  8544  oaword  8546  omcan  8566  omwordri  8569  odi  8576  omeulem1  8579  oeord  8585  oecan  8586  oewordri  8589  oeordsuc  8591  nnaord  8616  nnaordr  8617  nndi  8620  nnaword  8624  nnmwordri  8633  naddel2  8684  naddss1  8685  naddss2  8686  erov  8805  ecopovtrn  8811  mapsnd  8877  f1dom3g  8960  xpdom3  9067  mapxpen  9140  dif1en  9157  dif1enOLD  9159  findcard  9160  f1domfi2  9182  entrfir  9191  domtrfil  9192  domtrfir  9194  sbthfilem  9198  sdomdomtrfi  9201  php3  9209  findcard3  9282  indexfi  9357  suppr  9463  infpr  9495  r111  9767  tcrank  9876  acndom  10043  infdif2  10202  infxpdom  10203  cfeq0  10248  cfsuc  10249  cfflb  10251  cflim2  10255  cfsmolem  10262  axcc3  10430  domtriomlem  10434  axdc3lem2  10443  axdc3lem4  10445  axdc4lem  10447  axcclem  10449  pwcfsdom  10575  tsktrss  10753  tsksuc  10754  tskuni  10775  adderpqlem  10946  mulerpqlem  10947  mulcanenq  10952  distrnq  10953  ltsonq  10961  ltanq  10963  ltmnq  10964  distrlem1pr  11017  distrlem5pr  11019  ltsopr  11024  ltsosr  11086  ltasr  11092  adddir  11202  axlttrn  11283  letr  11305  nnncan1  11493  npncan3  11495  pnpcan2  11497  subdi  11644  subdir  11645  mulcan1g  11864  mulcan2g  11865  divmul  11872  div23  11888  div13  11890  muldivdir  11904  divsubdir  11905  subdivcomb1  11906  divcan7  11920  ltmul2  12062  lemul1  12063  lemul2  12064  lemul2a  12066  lediv1  12076  ltmuldiv2  12085  lemuldiv  12091  lemuldiv2  12092  ltdiv2  12097  lediv2  12101  infrelb  12196  nndivtr  12256  bndndx  12468  nn0n0n1ge2  12536  fnn0ind  12658  addlelt  13085  xrletr  13134  qsqueeze  13177  xleadd2a  13230  xleadd1  13231  xltadd2  13233  xltmul2  13269  supxrbnd  13304  iooneg  13445  iccneg  13446  icoshft  13447  icoshftf1o  13448  zltaddlt1le  13479  fzen  13515  uzsubsubfz  13520  ssfzunsnext  13543  fzrevral2  13584  fzshftral  13586  fz0fzdiffz0  13607  elfzmlbp  13609  elfzo  13631  nelfzo  13634  fzoaddel2  13685  fzosubel2  13689  ssfzo12bi  13724  fzonfzoufzol  13732  subfzo0  13751  flltdivnn0lt  13795  modmulnn  13851  modcyc  13868  modaddabs  13871  modaddmod  13872  modmuladd  13875  modadd2mod  13883  modsubmod  13891  modsubmodmod  13892  modaddmodup  13896  modmulmod  13898  modsubdir  13902  modfzo0difsn  13905  modsumfzodifsn  13906  uzindi  13944  axdc4uzlem  13945  expneg2  14033  expdiv  14076  expubnd  14139  mulbinom2  14183  bernneq2  14190  expnngt1  14201  hashinfxadd  14342  hashunsngx  14350  hashunsnggt  14351  hashfundm  14399  hashdifsnp1  14454  ccatval3  14526  ccatfv0  14530  ccatval1lsw  14531  ccats1val2  14574  ccatw2s1p1  14583  swrdnd  14601  pfxsuffeqwrdeq  14645  pfxsuff1eqwrdeq  14646  swrdswrd  14652  pfxpfx  14655  wrd2ind  14670  swrdccatin1  14672  pfxccatin12lem1  14675  swrdccatin2  14676  pfxccatin12lem3  14679  swrdccat  14682  pfxccatpfx1  14683  pfxccatpfx2  14684  swrdccat3blem  14686  repswswrd  14731  repswpfx  14732  repswccat  14733  cshwidxmod  14750  2cshw  14760  3cshw  14765  scshwfzeqfzo  14774  cshwcsh2id  14776  cshimadifsn  14777  cshimadifsn0  14778  ccatco  14783  cshco  14784  swrdco  14785  pfxco  14786  lswco  14787  swrds2  14888  2swrd2eqwrdeq  14901  shftuz  15013  abs3dif  15275  fsumdifsnconst  15734  modfsummods  15736  sin02gt0  16132  dvdsval2  16197  dvdscmul  16223  dvdsmulc  16224  dvdscmulr  16225  dvdsmulcr  16226  divalglem8  16340  ndvdssub  16349  rpmulgcd  16495  coprmprod  16595  cncongr1  16601  cncongr2  16602  isprm3  16617  modprm0  16735  coprimeprodsq  16738  pythagtriplem12  16756  pythagtriplem14  16758  pcprendvds  16770  pcmul  16781  pcdiv  16782  pcqcl  16786  pcqdiv  16787  pcdvdsb  16799  vdwnnlem1  16925  hashbcss  16934  cshwshashlem1  17026  fvsetsid  17098  setsstruct2  17104  setsstruct  17106  mrcss  17557  mrcsscl  17561  mrcun  17563  cofulid  17837  catcisolem  18057  funcsetcestrclem9  18112  latleeqj1  18401  lubun  18465  clatleglb  18468  pslem  18522  dirtr  18552  mgmb1mgm1  18571  pwspjmhm  18708  grpinvid1  18873  grpinvid2  18874  grpasscan1  18883  grpasscan2  18884  grpinvadd  18898  grpsubf  18899  grpsubrcan  18901  grpinvsub  18902  grpsubeq0  18906  grpsubadd0sub  18907  grppncan  18911  grpnpcan  18912  mulgnn0p1  18960  mulgaddcomlem  18972  mulginvcom  18974  mulginvinv  18975  subgsubcl  19012  subgsub  19013  eqglact  19054  qussub  19065  ghmsub  19095  psgnunilem4  19360  oddvds2  19429  odsubdvds  19434  gexnnod  19451  slwn0  19478  dvrcl  20211  unitdvcl  20212  dvrcan1  20216  dvrcan3  20217  dvreq1  20218  subrgdv  20373  abvsubtri  20436  idsrngd  20463  lmodvsubval2  20520  lsmcl  20687  lsmsp2  20691  lspsntrim  20702  lidldvgen  20886  chrcong  21073  zndvds  21097  zntoslem  21104  ocvsscon  21220  obselocv  21275  frlmphl  21328  ascldimul  21434  mpfsubrg  21658  ply1tmcl  21786  eqcoe1ply1eq  21813  gsummoncoe1  21820  lply1binomsc  21823  mamudm  21882  mamufacex  21883  scmatf1  22025  scmatf1o  22026  scmatrngiso  22030  submabas  22072  mdetdiaglem  22092  mdetralt2  22103  mdetero  22104  mdetunilem2  22107  mdetunilem6  22111  m2detleiblem7  22121  maducoeval2  22134  gsummatr01lem3  22151  gsummatr01  22153  smadiadetglem2  22166  cramerlem1  22181  mply1topmatcl  22299  mp2pm2mplem4  22303  ntrin  22557  elnei  22607  neindisj2  22619  ordtopn3  22692  leordtval2  22708  lecldbas  22715  cnrest2  22782  cmpsublem  22895  ptrescn  23135  xkococn  23156  kqfeq  23220  snfbas  23362  neifil  23376  fclsrest  23520  utopsnnei  23746  neipcfilu  23793  psmetsym  23808  psmetge0  23810  xmetge0  23842  xmetsym  23845  metustto  24054  metustbl  24067  restmetu  24071  nm2dif  24126  nmtri  24127  cnmet  24280  cnmpopc  24436  iihalf1  24439  iihalf2  24441  iocopnst  24448  clmnegsubdi2  24613  clmsub4  24614  clmvsubval2  24618  ncvspi  24665  cphsqrtcl3  24696  cph2ass  24722  cphipval2  24750  cphipval  24752  caublcls  24818  bcthlem3  24835  bcthlem4  24836  srabn  24869  cssbn  24884  cmslsschl  24886  rrxmet  24917  rrxdsfi  24920  iblconst  25327  tdeglem3OLD  25568  dvdsq1p  25670  coeid3  25746  aannenlem2  25834  pserdvlem2  25932  tanord1  26038  cxpef  26165  recxpcl  26175  logbchbase  26266  relogbcl  26268  relogbzcl  26269  logbleb  26278  logblt  26279  relogbcxpb  26282  lawcos  26311  pythag  26312  isosctrlem1  26313  isosctrlem2  26314  lgsmodeq  26835  lgsmulsqcoprm  26836  gausslemma2dlem1a  26858  2lgsoddprmlem2  26902  sltres  27155  sletr  27251  cofcutr  27401  lrrecpo  27415  sltadd2im  27459  sleadd2im  27461  sleadd1  27462  sleadd2  27463  sltadd1  27465  addscan2  27466  addscan1  27467  sltsub1  27533  divsmulw  27630  ax5seglem1  28176  axcontlem2  28213  axcontlem8  28219  upgrpredgv  28389  numedglnl  28394  issubgr2  28519  uhgrissubgr  28522  egrsubgr  28524  nbusgrfi  28621  nb3grprlem2  28628  cplgr3v  28682  cusgrsizeindslem  28698  finsumvtxdg2size  28797  rusgrpropadjvtx  28832  upgrwlkvtxedg  28892  usgr2trlncl  29007  uspgrn2crct  29052  crctcshwlkn0lem4  29057  crctcshwlkn0lem5  29058  wwlksnextproplem3  29155  umgr2adedgwlklem  29188  rusgr0edg  29217  clwwlk1loop  29231  clwwlkccatlem  29232  clwlkclwwlklem2a4  29240  clwlkclwwlklem2a  29241  clwwisshclwwslemlem  29256  erclwwlktr  29265  clwwlkel  29289  erclwwlkntr  29314  clwwlknonex2lem2  29351  uhgr3cyclex  29425  umgr3cyclex  29426  eucrctshift  29486  frgr3v  29518  3cyclfrgrrn  29529  frgrwopreglem5a  29554  frgr2wsp1  29573  extwwlkfab  29595  clwwlknonclwlknonf1o  29605  numclwwlk3lem1  29625  numclwwlk5  29631  numclwwlk6  29633  isgrpo  29738  grpoinvid1  29769  grpoinvid2  29770  grpoinvop  29774  grpodivinv  29777  grpoinvdiv  29778  grpodivf  29779  grponpcan  29784  ablonncan  29797  nvmval  29883  nvmval2  29884  nvmfval  29885  nvmul0or  29891  nvpncan2  29894  nvaddsub4  29898  nvmeq0  29899  nvdif  29907  nvpi  29908  nvmtri  29912  nvabs  29913  imsmetlem  29931  ipval2lem3  29946  ipval2  29948  4ipval2  29949  ipval3  29950  nmooge0  30008  blometi  30044  hvaddsub12  30279  hvsubdistr1  30290  hvsubdistr2  30291  hvaddcan2  30312  hvmulcan  30313  hvmulcan2  30314  hvsubcan  30315  hvsubcan2  30316  his7  30331  his2sub  30333  his2sub2  30334  norm3dif2  30392  shsubcl  30461  hhssnv  30505  shlej2  30602  fh2  30860  cm2j  30861  pjoi0  30958  hodcl  30988  hosubdi  31049  unopf1o  31157  unopadj  31160  adj2  31175  braadd  31186  bramul  31187  lnopaddmuli  31214  lnopsubmuli  31216  homco2  31218  lnfnaddmuli  31286  adjlnop  31327  leopmul  31375  leoptr  31378  pjimai  31417  atcv1  31621  atexch  31622  atcvatlem  31626  fcoinvbr  31824  preiman0  31919  divnumden2  32012  xdivmul  32079  cshf1o  32114  dvdschrmulg  32369  resvsca  32433  idlsrgcmnd  32618  hasheuni  33072  difelsiga  33120  cndprobin  33422  bayesth  33427  sgn3da  33529  signstfvp  33571  breprexplemc  33633  fineqvac  34086  hashf1dmcdm  34094  swrdrevpfx  34096  swrdwlk  34106  lediv2aALT  34651  fununiq  34729  dfrdg2  34756  clsun  35202  neiin  35206  rdgeqoa  36240  curfv  36457  matunitlindflem1  36473  poimirlem32  36509  ftc1anclem4  36553  areacirc  36570  filbcmb  36597  ismtybnd  36664  grpoeqdivid  36738  ghomco  36748  rngonegrmul  36801  zerdivemp1x  36804  rngohomco  36831  rngoisoco  36839  riscer  36845  intidl  36886  isfldidl  36925  brredunds  37485  lshpnelb  37843  opnlen0  38047  opcon3b  38055  opcon2b  38056  oplecon3b  38059  opltcon3b  38063  opltcon2b  38065  oldmm1  38076  oldmm4  38079  oldmj1  38080  oldmj4  38083  cvrval2  38133  cvrcon3b  38136  leatb  38151  atcmp  38170  atcvreq0  38173  atlatle  38179  athgt  38316  3dim2  38328  islln2a  38377  lplnnleat  38402  lvolnleat  38443  4atlem10  38466  4atlem11  38469  4atlem12  38472  dalem21  38554  dalem22  38555  dalem23  38556  dalem29  38561  dalem30  38562  dalem31N  38563  dalem32  38564  dalem33  38565  dalem34  38566  dalem35  38567  dalem36  38568  dalem37  38569  dalem40  38572  dalem46  38578  dalem47  38579  dalem51  38583  dalem52  38584  dalem58  38590  dalem59  38591  pmaple  38621  paddclN  38702  pmapjoin  38712  pmapjat1  38713  elpcliN  38753  pclssN  38754  pclun2N  38759  2polcon4bN  38778  paddunN  38787  poldmj1N  38788  pmapj2N  38789  pmapocjN  38790  psubclinN  38808  paddatclN  38809  poml4N  38813  lautco  38957  ldilco  38976  ltrneq2  39008  trljat1  39026  cdlemc1  39051  cdleme10  39114  ltrnco  39579  trlcocnv  39580  trljco  39600  trljco2  39601  cdlemi1  39678  tendocnv  39881  diaord  39907  dibord  40019  dihord3  40117  dihord4  40118  dihmeetlem2N  40159  dihmeetlem4preN  40166  dochdmj1  40250  hdmap10lem  40699  lcmineqlem1  40883  sticksstones2  40952  metakunt29  41002  metakunt30  41003  factwoffsmonot  41012  dvdsexpim  41215  expgcd  41221  zexpgcd  41223  readdsub  41254  reltsub1  41256  renpncan3  41261  reppncan  41263  resubdi  41266  readdcan2  41282  mzprename  41473  dvdsrabdioph  41534  pell14qrdivcl  41589  monotoddzz  41668  jm2.19lem2  41715  jm2.19  41718  relexpaddss  42455  k0004lem3  42886  dvconstbi  43079  chordthmALT  43680  isosctrlem1ALT  43681  ssinc  43762  ssdec  43763  wessf1ornlem  43868  disjf1o  43875  ssnnf1octb  43879  projf1o  43882  mapssbi  43898  iunmapsn  43902  upbdrech  44002  iuneqfzuzlem  44031  suplesup  44036  rexabslelem  44115  climxrrelem  44452  limsupresxr  44469  liminfresxr  44470  liminfvalxr  44486  xlimliminflimsup  44565  cncfshift  44577  cncfperiod  44582  cncfuni  44589  icccncfext  44590  dvmptfprodlem  44647  dvnprodlem1  44649  itgspltprt  44682  ismbl3  44689  stoweidlem3  44706  stoweidlem10  44713  stoweidlem19  44722  stoweidlem31  44734  stoweidlem34  44737  stoweidlem44  44747  fourierdlem41  44851  fourierdlem42  44852  fourierdlem51  44860  fourierdlem68  44877  fourierdlem89  44898  fourierdlem91  44900  fourierdlem92  44901  fourierdlem94  44903  etransclem24  44961  etransclem34  44971  qndenserrnbllem  44997  salincl  45027  saldifcl2  45031  subsalsal  45062  sge0pr  45097  sge0pnffigt  45099  sge0reuz  45150  nnfoctbdjlem  45158  nnfoctbdj  45159  meadjiunlem  45168  caratheodorylem2  45230  hoidmv1le  45297  hoidmvlelem3  45300  hspmbllem2  45330  opnvonmbllem2  45336  sssmf  45441  smfaddlem1  45466  sigaraf  45556  sigarmf  45557  nltle2tri  46008  subsubelfzo0  46021  iccpartiltu  46077  icceuelpart  46091  poprelb  46179  reuopreuprim  46181  proththd  46269  mogoldbblem  46375  fppr2odd  46386  fpprel2  46396  bgoldbtbndlem2  46461  isomgrtr  46494  rngisom1  46704  rngisomring  46705  rngqiprngimfolem  46756  nn0sumltlt  46980  invginvrid  46997  ply1sclrmsm  47018  linccl  47049  lincvalpr  47053  lincresunit3lem1  47114  lincresunit3  47116  fdivmpt  47180  nnolog2flm1  47230  dignnld  47243  digexp  47247  dignn0flhalflem1  47255  itcovalsucov  47308  reorelicc  47350  eenglngeehlnmlem1  47377  line2  47392  line2xlem  47393  itsclc0lem1  47396  itsclc0xyqsolr  47409  i0oii  47506  io1ii  47507  indthinc  47626  indthincALT  47627  setrec2fun  47691  reccot  47757  rectan  47758