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

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

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 1088

This theorem is referenced by:  3ad2ant1  1133  3simpb  1149  3imp3i2an  1346  eupickb  2629  vtoclegftOLD  3558  eqeu  3680  onunel  6442  iotan0  6504  funopg  6553  dff1o2  6808  fvelimad  6931  unima  6939  fnimapr  6947  fvmptt  6991  fnreseql  7023  xpprsng  7115  f1elima  7241  f1ounsn  7250  f13dfv  7252  f1ocnvfvb  7257  f1cdmsn  7260  f1ofvswap  7284  oprssov  7561  resf1extb  7913  resf1ext2b  7914  funelss  8029  poxp  8110  poxp2  8125  poxp3  8132  smoiso  8334  oaord  8514  oaword  8516  omcan  8536  omwordri  8539  odi  8546  omeulem1  8549  oeord  8555  oecan  8556  oewordri  8559  oeordsuc  8561  nnaord  8586  nnaordr  8587  nndi  8590  nnaword  8594  nnmwordri  8603  naddel2  8655  naddss1  8656  naddss2  8657  erov  8790  ecopovtrn  8796  mapsnd  8862  f1dom3g  8942  xpdom3  9044  mapxpen  9113  dif1en  9130  dif1enOLD  9132  findcard  9133  f1domfi2  9152  entrfir  9161  domtrfil  9162  domtrfir  9164  sbthfilem  9168  sdomdomtrfi  9171  php3  9179  findcard3  9236  indexfi  9318  suppr  9430  infpr  9463  r111  9735  tcrank  9844  acndom  10011  infdif2  10169  infxpdom  10170  cfeq0  10216  cfsuc  10217  cfflb  10219  cflim2  10223  cfsmolem  10230  axcc3  10398  domtriomlem  10402  axdc3lem2  10411  axdc3lem4  10413  axdc4lem  10415  axcclem  10417  pwcfsdom  10543  tsktrss  10721  tsksuc  10722  tskuni  10743  adderpqlem  10914  mulerpqlem  10915  mulcanenq  10920  distrnq  10921  ltsonq  10929  ltanq  10931  ltmnq  10932  distrlem1pr  10985  distrlem5pr  10987  ltsopr  10992  ltsosr  11054  ltasr  11060  adddir  11172  axlttrn  11253  letr  11275  nnncan1  11465  npncan3  11467  pnpcan2  11469  subdi  11618  subdir  11619  mulcan1g  11838  mulcan2g  11839  divmul  11847  div23  11863  div13  11865  muldivdir  11882  divsubdir  11883  subdivcomb1  11884  divcan7  11898  ltmul2  12040  lemul1  12041  lemul2  12042  lemul2a  12044  lediv1  12055  ltmuldiv2  12064  lemuldiv  12070  lemuldiv2  12071  ltdiv2  12076  lediv2  12080  infrelb  12175  nndivtr  12240  bndndx  12448  nn0n0n1ge2  12517  fnn0ind  12640  addlelt  13074  xrletr  13125  qsqueeze  13168  xleadd2a  13221  xleadd1  13222  xltadd2  13224  xltmul2  13260  supxrbnd  13295  iooneg  13439  iccneg  13440  icoshft  13441  icoshftf1o  13442  zltaddlt1le  13473  fzen  13509  uzsubsubfz  13514  ssfzunsnext  13537  fzrevral2  13581  fzshftral  13583  fz0fzdiffz0  13605  elfzmlbp  13607  elfzo  13629  nelfzo  13632  fzoaddel2  13688  fzosubel2  13693  ssfzo12bi  13729  fzonfzoufzol  13738  subfzo0  13757  flltdivnn0lt  13802  modmulnn  13858  modcyc  13875  modaddabs  13880  modaddmod  13881  modmuladd  13885  modadd2mod  13893  modsubmod  13901  modsubmodmod  13902  modaddmodup  13906  modmulmod  13908  modsubdir  13912  modfzo0difsn  13915  modsumfzodifsn  13916  uzindi  13954  axdc4uzlem  13955  expneg2  14042  expdiv  14085  expubnd  14150  mulbinom2  14195  bernneq2  14202  expnngt1  14213  hashinfxadd  14357  hashunsngx  14365  hashunsnggt  14366  hashfundm  14414  hashf1dmcdm  14416  hashdifsnp1  14478  ccatval3  14551  ccatfv0  14555  ccatval1lsw  14556  ccats1val2  14599  ccatw2s1p1  14608  swrdnd  14626  pfxsuffeqwrdeq  14670  pfxsuff1eqwrdeq  14671  swrdswrd  14677  pfxpfx  14680  wrd2ind  14695  swrdccatin1  14697  pfxccatin12lem1  14700  swrdccatin2  14701  pfxccatin12lem3  14704  swrdccat  14707  pfxccatpfx1  14708  pfxccatpfx2  14709  swrdccat3blem  14711  repswswrd  14756  repswpfx  14757  repswccat  14758  cshwidxmod  14775  2cshw  14785  3cshw  14790  scshwfzeqfzo  14799  cshwcsh2id  14801  cshimadifsn  14802  cshimadifsn0  14803  ccatco  14808  cshco  14809  swrdco  14810  pfxco  14811  lswco  14812  swrds2  14913  2swrd2eqwrdeq  14926  shftuz  15042  abs3dif  15305  fsumdifsnconst  15764  modfsummods  15766  sin02gt0  16167  dvdsval2  16232  dvdscmul  16259  dvdsmulc  16260  dvdscmulr  16261  dvdsmulcr  16262  divalglem8  16377  ndvdssub  16386  dvdsexpim  16532  rpmulgcd  16534  expgcd  16540  zexpgcd  16542  coprmprod  16638  cncongr1  16644  cncongr2  16645  isprm3  16660  modprm0  16783  coprimeprodsq  16786  pythagtriplem12  16804  pythagtriplem14  16806  pcprendvds  16818  pcmul  16829  pcdiv  16830  pcqcl  16834  pcqdiv  16835  pcdvdsb  16847  vdwnnlem1  16973  hashbcss  16982  cshwshashlem1  17073  fvsetsid  17145  setsstruct2  17151  setsstruct  17153  mrcss  17584  mrcsscl  17588  mrcun  17590  cofulid  17859  catcisolem  18079  funcsetcestrclem9  18131  latleeqj1  18417  lubun  18481  clatleglb  18484  pslem  18538  dirtr  18568  mgmb1mgm1  18589  pwspjmhm  18764  grpinvid1  18930  grpinvid2  18931  grpasscan1  18940  grpasscan2  18941  grpinvadd  18957  grpsubf  18958  grpsubrcan  18960  grpinvsub  18961  grpsubeq0  18965  grpsubadd0sub  18966  grppncan  18970  grpnpcan  18971  mulgnn0p1  19024  mulgaddcomlem  19036  mulginvcom  19038  mulginvinv  19039  subgsubcl  19076  subgsub  19077  eqglact  19118  qussub  19130  ghmsub  19163  psgnunilem4  19434  oddvds2  19503  odsubdvds  19508  gexnnod  19525  slwn0  19552  dvrcl  20320  unitdvcl  20321  dvrcan1  20325  dvrcan3  20326  dvreq1  20327  rngisom1  20382  rngisomring  20383  subrgdv  20505  abvsubtri  20743  idsrngd  20772  lmodvsubval2  20830  lsmcl  20997  lsmsp2  21001  lspsntrim  21012  rngqiprngimfolem  21207  lidldvgen  21251  cncrng  21307  chrcong  21444  dvdschrmulg  21445  zndvds  21466  zntoslem  21473  ocvsscon  21591  obselocv  21644  frlmphl  21697  ascldimul  21804  mpfsubrg  22017  ply1tmcl  22165  eqcoe1ply1eq  22193  gsummoncoe1  22202  lply1binomsc  22205  mamudm  22289  mamufacex  22290  scmatf1  22425  scmatf1o  22426  scmatrngiso  22430  submabas  22472  mdetdiaglem  22492  mdetralt2  22503  mdetero  22504  mdetunilem2  22507  mdetunilem6  22511  m2detleiblem7  22521  maducoeval2  22534  gsummatr01lem3  22551  gsummatr01  22553  smadiadetglem2  22566  cramerlem1  22581  mply1topmatcl  22699  mp2pm2mplem4  22703  ntrin  22955  elnei  23005  neindisj2  23017  ordtopn3  23090  leordtval2  23106  lecldbas  23113  cnrest2  23180  cmpsublem  23293  ptrescn  23533  xkococn  23554  kqfeq  23618  snfbas  23760  neifil  23774  fclsrest  23918  utopsnnei  24144  neipcfilu  24190  psmetsym  24205  psmetge0  24207  xmetge0  24239  xmetsym  24242  metustto  24448  metustbl  24461  restmetu  24465  nm2dif  24520  nmtri  24521  cnmet  24666  cnmpopc  24829  iihalf1  24832  iihalf2  24835  iocopnst  24844  clmnegsubdi2  25012  clmsub4  25013  clmvsubval2  25017  ncvspi  25063  cphsqrtcl3  25094  cph2ass  25120  cphipval2  25148  cphipval  25150  caublcls  25216  bcthlem3  25233  bcthlem4  25234  srabn  25267  cssbn  25282  cmslsschl  25284  rrxmet  25315  rrxdsfi  25318  iblconst  25726  dvdsq1p  26075  coeid3  26152  aannenlem2  26244  pserdvlem2  26345  tanord1  26453  cxpef  26581  recxpcl  26591  logbchbase  26688  relogbcl  26690  relogbzcl  26691  logbleb  26700  logblt  26701  relogbcxpb  26704  lawcos  26733  pythag  26734  isosctrlem1  26735  isosctrlem2  26736  lgsmodeq  27260  lgsmulsqcoprm  27261  gausslemma2dlem1a  27283  2lgsoddprmlem2  27327  sltres  27581  sletr  27677  cofcutr  27839  lrrecpo  27855  sltadd2im  27900  sleadd2im  27902  sleadd1  27903  sleadd2  27904  sltadd1  27906  addscan2  27907  addscan1  27908  sltsub1  27987  divsmulw  28103  ax5seglem1  28862  axcontlem2  28899  axcontlem8  28905  upgrpredgv  29073  numedglnl  29078  issubgr2  29206  uhgrissubgr  29209  egrsubgr  29211  nbusgrfi  29308  nb3grprlem2  29315  cplgr3v  29369  cusgrsizeindslem  29386  finsumvtxdg2size  29485  rusgrpropadjvtx  29520  upgrwlkvtxedg  29580  usgr2trlncl  29697  uspgrn2crct  29745  crctcshwlkn0lem4  29750  crctcshwlkn0lem5  29751  wwlksnextproplem3  29848  umgr2adedgwlklem  29881  rusgr0edg  29910  clwwlk1loop  29924  clwwlkccatlem  29925  clwlkclwwlklem2a4  29933  clwlkclwwlklem2a  29934  clwwisshclwwslemlem  29949  erclwwlktr  29958  clwwlkel  29982  erclwwlkntr  30007  clwwlknonex2lem2  30044  uhgr3cyclex  30118  umgr3cyclex  30119  eucrctshift  30179  frgr3v  30211  3cyclfrgrrn  30222  frgrwopreglem5a  30247  frgr2wsp1  30266  extwwlkfab  30288  clwwlknonclwlknonf1o  30298  numclwwlk3lem1  30318  numclwwlk5  30324  numclwwlk6  30326  isgrpo  30433  grpoinvid1  30464  grpoinvid2  30465  grpoinvop  30469  grpodivinv  30472  grpoinvdiv  30473  grpodivf  30474  grponpcan  30479  ablonncan  30492  nvmval  30578  nvmval2  30579  nvmfval  30580  nvmul0or  30586  nvpncan2  30589  nvaddsub4  30593  nvmeq0  30594  nvdif  30602  nvpi  30603  nvmtri  30607  nvabs  30608  imsmetlem  30626  ipval2lem3  30641  ipval2  30643  4ipval2  30644  ipval3  30645  nmooge0  30703  blometi  30739  hvaddsub12  30974  hvsubdistr1  30985  hvsubdistr2  30986  hvaddcan2  31007  hvmulcan  31008  hvmulcan2  31009  hvsubcan  31010  hvsubcan2  31011  his7  31026  his2sub  31028  his2sub2  31029  norm3dif2  31087  shsubcl  31156  hhssnv  31200  shlej2  31297  fh2  31555  cm2j  31556  pjoi0  31653  hodcl  31683  hosubdi  31744  unopf1o  31852  unopadj  31855  adj2  31870  braadd  31881  bramul  31882  lnopaddmuli  31909  lnopsubmuli  31911  homco2  31913  lnfnaddmuli  31981  adjlnop  32022  leopmul  32070  leoptr  32073  pjimai  32112  atcv1  32316  atexch  32317  atcvatlem  32321  fcoinvbr  32541  preiman0  32640  divnumden2  32747  sgn3da  32766  xdivmul  32852  cshf1o  32891  resvsca  33311  idlsrgcmnd  33493  hasheuni  34082  difelsiga  34130  cndprobin  34432  bayesth  34437  signstfvp  34569  breprexplemc  34630  fineqvac  35094  swrdrevpfx  35111  swrdwlk  35121  lediv2aALT  35671  fununiq  35763  dfrdg2  35790  clsun  36323  neiin  36327  rdgeqoa  37365  curfv  37601  matunitlindflem1  37617  poimirlem32  37653  ftc1anclem4  37697  areacirc  37714  filbcmb  37741  ismtybnd  37808  grpoeqdivid  37882  ghomco  37892  rngonegrmul  37945  zerdivemp1x  37948  rngohomco  37975  rngoisoco  37983  riscer  37989  intidl  38030  isfldidl  38069  eceldmqsxrncnvepres  38405  eceldmqsxrncnvepres2  38406  brredunds  38624  lshpnelb  38984  opnlen0  39188  opcon3b  39196  opcon2b  39197  oplecon3b  39200  opltcon3b  39204  opltcon2b  39206  oldmm1  39217  oldmm4  39220  oldmj1  39221  oldmj4  39224  cvrval2  39274  cvrcon3b  39277  leatb  39292  atcmp  39311  atcvreq0  39314  atlatle  39320  athgt  39457  3dim2  39469  islln2a  39518  lplnnleat  39543  lvolnleat  39584  4atlem10  39607  4atlem11  39610  4atlem12  39613  dalem21  39695  dalem22  39696  dalem23  39697  dalem29  39702  dalem30  39703  dalem31N  39704  dalem32  39705  dalem33  39706  dalem34  39707  dalem35  39708  dalem36  39709  dalem37  39710  dalem40  39713  dalem46  39719  dalem47  39720  dalem51  39724  dalem52  39725  dalem58  39731  dalem59  39732  pmaple  39762  paddclN  39843  pmapjoin  39853  pmapjat1  39854  elpcliN  39894  pclssN  39895  pclun2N  39900  2polcon4bN  39919  paddunN  39928  poldmj1N  39929  pmapj2N  39930  pmapocjN  39931  psubclinN  39949  paddatclN  39950  poml4N  39954  lautco  40098  ldilco  40117  ltrneq2  40149  trljat1  40167  cdlemc1  40192  cdleme10  40255  ltrnco  40720  trlcocnv  40721  trljco  40741  trljco2  40742  cdlemi1  40819  tendocnv  41022  diaord  41048  dibord  41160  dihord3  41258  dihord4  41259  dihmeetlem2N  41300  dihmeetlem4preN  41307  dochdmj1  41391  hdmap10lem  41840  lcmineqlem1  42024  sticksstones2  42142  readdsub  42379  reltsub1  42381  renpncan3  42386  reppncan  42388  resubdi  42391  readdcan2  42408  mzprename  42744  dvdsrabdioph  42805  pell14qrdivcl  42860  monotoddzz  42939  jm2.19lem2  42986  jm2.19  42989  relexpaddss  43714  k0004lem3  44145  dvconstbi  44330  chordthmALT  44929  isosctrlem1ALT  44930  ssinc  45088  ssdec  45089  wessf1ornlem  45186  disjf1o  45192  ssnnf1octb  45195  projf1o  45198  mapssbi  45214  iunmapsn  45218  upbdrech  45310  iuneqfzuzlem  45337  suplesup  45342  rexabslelem  45421  climxrrelem  45754  limsupresxr  45771  liminfresxr  45772  liminfvalxr  45788  xlimliminflimsup  45867  cncfshift  45879  cncfperiod  45884  cncfuni  45891  icccncfext  45892  dvmptfprodlem  45949  dvnprodlem1  45951  itgspltprt  45984  ismbl3  45991  stoweidlem3  46008  stoweidlem10  46015  stoweidlem19  46024  stoweidlem31  46036  stoweidlem34  46039  stoweidlem44  46049  fourierdlem41  46153  fourierdlem42  46154  fourierdlem51  46162  fourierdlem68  46179  fourierdlem89  46200  fourierdlem91  46202  fourierdlem92  46203  fourierdlem94  46205  etransclem24  46263  etransclem34  46273  qndenserrnbllem  46299  salincl  46329  saldifcl2  46333  subsalsal  46364  sge0pr  46399  sge0pnffigt  46401  sge0reuz  46452  nnfoctbdjlem  46460  nnfoctbdj  46461  meadjiunlem  46470  caratheodorylem2  46532  hoidmv1le  46599  hoidmvlelem3  46602  hspmbllem2  46632  opnvonmbllem2  46638  sssmf  46743  smfaddlem1  46768  sigaraf  46858  sigarmf  46859  nltle2tri  47318  subsubelfzo0  47331  submodaddmod  47346  zplusmodne  47348  addmodne  47349  minusmod5ne  47354  submodneaddmod  47356  modmkpkne  47366  modmknepk  47367  iccpartiltu  47427  icceuelpart  47441  poprelb  47529  reuopreuprim  47531  proththd  47619  mogoldbblem  47725  fppr2odd  47736  fpprel2  47746  bgoldbtbndlem2  47811  clnbusgrfi  47847  grimuhgr  47891  uhgrimisgrgric  47935  clnbgrgrim  47938  grtrif1o  47945  grlimgrtri  47999  gpgusgralem  48051  gpgedgvtx0  48056  gpgedg2ov  48061  gpgedg2iv  48062  gpg5nbgrvtx03starlem2  48064  nn0sumltlt  48342  invginvrid  48359  ply1sclrmsm  48376  linccl  48407  lincvalpr  48411  lincresunit3lem1  48472  lincresunit3  48474  fdivmpt  48533  nnolog2flm1  48583  dignnld  48596  digexp  48600  dignn0flhalflem1  48608  itcovalsucov  48661  reorelicc  48703  eenglngeehlnmlem1  48730  line2  48745  line2xlem  48746  itsclc0lem1  48749  itsclc0xyqsolr  48762  i0oii  48912  io1ii  48913  indthinc  49455  indthincALT  49456  setrec2fun  49685  reccot  49751  rectan  49752