Theorem 3adant2 1154

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

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1100

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 198  df-an 385  df-3an 1102

This theorem is referenced by:  3ad2ant1  1156  3simpb  1173  3imp3i2an  1445  eupickb  2699  vtoclegft  3469  eqeu  3569  funopg  6129  fnco  6204  dff1o2  6352  fnimapr  6477  fvmptt  6515  fnreseql  6543  f1elima  6738  f13dfv  6748  f1ocnvfvb  6753  oprssov  7027  ordunel  7251  poxp  7517  wfrlem4  7647  wfrlem4OLD  7648  smoiso  7689  oaord  7858  oaword  7860  omcan  7880  omwordri  7883  odi  7890  omeulem1  7893  oeord  7899  oecan  7900  oewordri  7903  oeordsuc  7905  nnaord  7930  nnaordr  7931  nndi  7934  nnaword  7938  nnmwordri  7947  erov  8074  ecopovtrn  8080  mapsnd  8128  xpdom3  8291  mapxpen  8359  findcard  8432  indexfi  8507  suppr  8610  infpr  8642  r111  8879  tcrank  8988  acndom  9151  infdif2  9311  infxpdom  9312  cfeq0  9357  cfsuc  9358  cfflb  9360  cflim2  9364  cfsmolem  9371  axcc3  9539  domtriomlem  9543  axdc3lem2  9552  axdc3lem4  9554  axdc4lem  9556  axcclem  9558  pwcfsdom  9684  tsktrss  9862  tsksuc  9863  tskuni  9884  adderpqlem  10055  mulerpqlem  10056  mulcanenq  10061  distrnq  10062  ltsonq  10070  ltanq  10072  ltmnq  10073  distrlem1pr  10126  distrlem5pr  10128  ltsopr  10133  ltsosr  10194  ltasr  10200  adddir  10310  axlttrn  10389  letr  10410  nnncan1  10596  npncan3  10598  pnpcan2  10600  subdi  10742  subdir  10743  mulcan1g  10959  mulcan2g  10960  divmul  10967  div23  10983  div13  10985  muldivdir  10999  divsubdir  11000  divcan7  11013  ltmul2  11153  lemul1  11154  lemul2  11155  lemul2a  11157  lediv1  11167  ltmuldiv2  11176  lemuldiv  11182  lemuldiv2  11183  ltdiv2  11188  lediv2  11192  fiminre  11251  infrelb  11287  nndivtr  11342  bndndx  11552  nn0n0n1ge2  11618  fnn0ind  11736  addlelt  12152  xrletr  12201  qsqueeze  12244  xleadd2a  12296  xleadd1  12297  xltadd2  12299  xltmul2  12335  supxrbnd  12370  iooneg  12507  iccneg  12508  icoshft  12509  icoshftf1o  12510  zltaddlt1le  12541  fzen  12575  uzsubsubfz  12580  ssfzunsnext  12603  fzrevral2  12643  fzshftral  12645  fz0fzdiffz0  12666  elfzmlbp  12668  elfzo  12690  nelfzo  12693  fzoaddel2  12742  fzosubel2  12746  elfzom1p1elfzo  12766  ssfzo12bi  12781  fzonfzoufzol  12789  subfzo0  12808  flltdivnn0lt  12852  modmulnn  12906  modcyc  12923  modaddabs  12926  modaddmod  12927  modmuladd  12930  modadd2mod  12938  modsubmod  12946  modsubmodmod  12947  modaddmodup  12951  modmulmod  12953  moddi  12956  modsubdir  12957  modfzo0difsn  12960  modsumfzodifsn  12961  uzindi  12999  axdc4uzlem  13000  expneg2  13086  expdiv  13128  expubnd  13138  mulbinom2  13201  bernneq2  13208  hashinfxadd  13386  hashdifsnp1  13489  ccatval3  13570  ccatsymb  13573  ccatfv0  13574  ccatval1lsw  13575  ccats1val2  13619  swrdnd  13650  2swrd1eqwrdeq  13672  swrdswrd  13678  wrd2ind  13695  swrdccatin1  13701  swrdccatin12lem2b  13704  swrdccatin2  13705  swrdccatin12lem2  13707  swrdccatin12lem3  13708  swrdccat  13711  swrdccat3a  13712  swrdccat3blem  13713  repswswrd  13749  repswccat  13750  cshwidxmod  13767  2cshw  13777  3cshw  13782  scshwfzeqfzo  13790  cshwcsh2id  13792  cshimadifsn  13793  cshimadifsn0  13794  ccatco  13799  cshco  13800  swrdco  13801  lswco  13802  swrds2  13903  2swrd2eqwrdeq  13915  shftuz  14026  shftval2  14032  abs3dif  14288  fsumdifsnconst  14739  modfsummods  14741  sin02gt0  15136  dvdsval2  15200  dvdscmul  15225  dvdsmulc  15226  dvdscmulr  15227  dvdsmulcr  15228  divalglem8  15337  ndvdssub  15346  rpmulgcd  15488  coprmprod  15587  cncongr1  15593  cncongr2  15594  isprm3  15608  modprm0  15721  coprimeprodsq  15724  pythagtriplem12  15742  pythagtriplem14  15744  pcprendvds  15756  pcmul  15767  pcdiv  15768  pcqcl  15772  pcqdiv  15773  pcdvdsb  15784  pcgcd  15793  vdwnnlem1  15910  hashbcss  15919  cshwshashlem1  16008  fvsetsid  16095  setsstruct2  16101  setsstruct  16103  mrcss  16475  mrcsscl  16479  mrcun  16481  cofulid  16748  catcisolem  16954  funcsetcestrclem9  17002  latleeqj1  17262  lubun  17322  clatleglb  17325  pslem  17405  dirtr  17435  mgmb1mgm1  17453  pwspjmhm  17567  gsumccat  17577  grpinvid1  17669  grpinvid2  17670  grpasscan1  17677  grpasscan2  17678  grpinvadd  17692  grpsubf  17693  grpsubrcan  17695  grpinvsub  17696  grpsubeq0  17700  grpsubadd0sub  17701  grppncan  17705  grpnpcan  17706  mulgnn0p1  17751  mulgaddcomlem  17761  mulginvcom  17763  mulginvinv  17764  subgsubcl  17801  subgsub  17802  eqglact  17841  qussub  17850  ghmsub  17864  psgnunilem4  18112  oddvds2  18178  odsubdvds  18181  gexnnod  18198  slwn0  18225  gsumdixp  18805  dvrcl  18882  unitdvcl  18883  dvrcan1  18887  dvrcan3  18888  dvreq1  18889  subrgdv  18995  abvsubtri  19033  idsrngd  19060  lmodvsubval2  19116  lsmcl  19284  lsmsp2  19288  lspsntrim  19299  lidldvgen  19458  evlslem4  19710  mpfsubrg  19734  ply1tmcl  19844  eqcoe1ply1eq  19869  gsummoncoe1  19876  lply1binomsc  19879  chrcong  20079  zndvds  20099  zntoslem  20106  ocvsscon  20223  obselocv  20276  frlmphl  20324  mamudm  20398  mamufacex  20399  scmatf1  20542  scmatf1o  20543  scmatrngiso  20547  submabas  20589  mdetdiaglem  20609  mdetralt2  20620  mdetero  20621  mdetunilem2  20624  mdetunilem6  20628  m2detleiblem7  20638  maducoeval2  20651  gsummatr01lem3  20669  gsummatr01  20671  smadiadetglem2  20684  cramerlem1  20700  mply1topmatcl  20817  mp2pm2mplem4  20821  ntrin  21073  elnei  21123  neindisj2  21135  ordtopn3  21208  ordtcld3  21211  leordtval2  21224  lecldbas  21231  cnrest2  21298  cmpsublem  21410  ptrescn  21650  xkococn  21671  kqfeq  21735  snfbas  21877  neifil  21891  fclsrest  22035  utopsnnei  22260  neipcfilu  22307  psmetsym  22322  psmetge0  22324  xmetge0  22356  xmetsym  22359  metustto  22565  metustbl  22578  restmetu  22582  nm2dif  22636  nmtri  22637  cnmet  22782  cnmpt2pc  22934  iihalf1  22937  iihalf2  22939  iocopnst  22946  clmnegsubdi2  23111  clmsub4  23112  clmvsubval2  23116  ncvspi  23162  cphsqrtcl3  23193  cph2ass  23219  cphipval2  23246  cphipval  23248  caublcls  23313  bcthlem3  23329  bcthlem4  23330  srabn  23362  rrxmet  23397  iblconst  23792  tdeglem3  24027  mdegmullem  24046  dvdsq1p  24128  coeid3  24204  aannenlem2  24292  pserdvlem2  24390  tanord1  24492  cxpef  24619  recxpcl  24629  logbchbase  24717  relogbcl  24719  relogbzcl  24720  logbleb  24729  logblt  24730  relogbcxpb  24733  lawcos  24754  pythag  24755  isosctrlem1  24756  isosctrlem2  24757  lgsmodeq  25275  lgsmulsqcoprm  25276  gausslemma2dlem1a  25298  2lgsoddprmlem2  25342  ax5seglem1  26016  axcontlem2  26053  axcontlem8  26059  upgrpredgv  26243  numedglnl  26248  issubgr2  26374  uhgrissubgr  26377  egrsubgr  26379  fusgrfisstep  26431  nbusgrfi  26486  nb3grprlem2  26493  cplgr3v  26553  cusgrsizeindslem  26569  finsumvtxdg2size  26668  rusgrpropadjvtx  26703  upgrwlkvtxedg  26763  usgr2trlncl  26878  uspgrn2crct  26923  crctcshwlkn0lem4  26928  crctcshwlkn0lem5  26929  wwlksnextproplem3  27043  umgr2adedgwlklem  27078  rusgr0edg  27109  clwwlk1loop  27125  clwwlkccatlem  27126  clwlkclwwlklem2a4  27134  clwlkclwwlklem2a  27135  clwwisshclwwslemlem  27150  erclwwlktr  27159  clwwlkel  27189  erclwwlkntr  27216  clwlksfclwwlkOLD  27230  clwwlknonwwlknonbOLD  27269  clwwlknonex2lem2  27271  uhgr3cyclex  27349  umgr3cyclex  27350  eucrctshift  27410  frgr3v  27444  3cyclfrgrrn  27455  frgrwopreglem5a  27480  frgr2wsp1  27499  extwwlkfab  27525  clwwlknonclwlknonf1o  27536  numclwwlk3lem1  27564  numclwwlk5  27570  numclwwlk6  27572  isgrpo  27674  grpoinvid1  27705  grpoinvid2  27706  grpoinvop  27710  grpodivinv  27713  grpoinvdiv  27714  grpodivf  27715  grponpcan  27720  ablonncan  27733  nvmval  27819  nvmval2  27820  nvmfval  27821  nvmul0or  27827  nvpncan2  27830  nvaddsub4  27834  nvmeq0  27835  nvdif  27843  nvpi  27844  nvmtri  27848  nvabs  27849  imsmetlem  27867  ipval2lem3  27882  ipval2  27884  4ipval2  27885  ipval3  27886  nmooge0  27944  blometi  27980  hvaddsub12  28217  hvsubdistr1  28228  hvsubdistr2  28229  hvaddcan2  28250  hvmulcan  28251  hvmulcan2  28252  hvsubcan  28253  hvsubcan2  28254  his7  28269  his2sub  28271  his2sub2  28272  norm3dif2  28330  shsubcl  28399  hhssnv  28443  shlej2  28542  fh2  28800  cm2j  28801  pjoi0  28898  hodcl  28928  hosubdi  28989  unopf1o  29097  unopadj  29100  adj2  29115  braadd  29126  bramul  29127  lnopaddmuli  29154  lnopsubmuli  29156  homco2  29158  lnfnaddmuli  29226  adjlnop  29267  leopmul  29315  leoptr  29318  pjimai  29357  atcv1  29561  atexch  29562  atcvatlem  29566  fcoinvbr  29738  divnumden2  29885  xdivmul  29952  resvsca  30149  hasheuni  30466  difelsiga  30515  cndprobin  30815  bayesth  30820  sgn3da  30922  breprexplemc  31029  lediv2aALT  31887  subdivcomb1  31927  fununiq  31983  dfrdg2  32015  sltres  32130  sletr  32198  clsun  32638  neiin  32642  rdgeqoa  33528  curfv  33696  matunitlindflem1  33712  poimirlem32  33748  ftc1anclem4  33794  areacirc  33811  filbcmb  33841  ismtybnd  33911  grpoeqdivid  33985  ghomco  33995  rngonegrmul  34048  zerdivemp1x  34051  rngohomco  34078  rngoisoco  34086  riscer  34092  intidl  34133  isfldidl  34172  lshpnelb  34758  opnlen0  34962  opcon3b  34970  opcon2b  34971  oplecon3b  34974  opltcon3b  34978  opltcon2b  34980  oldmm1  34991  oldmm4  34994  oldmj1  34995  oldmj4  34998  cvrval2  35048  cvrcon3b  35051  leatb  35066  atcmp  35085  atcvreq0  35088  atlatle  35094  athgt  35230  3dim2  35242  islln2a  35291  lplnnleat  35316  lvolnleat  35357  4atlem10  35380  4atlem11  35383  4atlem12  35386  dalem21  35468  dalem22  35469  dalem23  35470  dalem29  35475  dalem30  35476  dalem31N  35477  dalem32  35478  dalem33  35479  dalem34  35480  dalem35  35481  dalem36  35482  dalem37  35483  dalem40  35486  dalem46  35492  dalem47  35493  dalem51  35497  dalem52  35498  dalem58  35504  dalem59  35505  pmaple  35535  paddclN  35616  pmapjoin  35626  pmapjat1  35627  elpcliN  35667  pclssN  35668  pclun2N  35673  2polcon4bN  35692  paddunN  35701  poldmj1N  35702  pmapj2N  35703  pmapocjN  35704  psubclinN  35722  paddatclN  35723  poml4N  35727  lautco  35871  ldilco  35890  ltrneq2  35922  trljat1  35941  cdlemc1  35966  cdleme10  36029  ltrnco  36494  trlcocnv  36495  trljco  36515  trljco2  36516  cdlemi1  36593  tendocnv  36796  diaord  36822  dibord  36934  dihord3  37032  dihord4  37033  dihmeetlem2N  37074  dihmeetlem4preN  37081  dochdmj1  37165  hdmap10lem  37614  mzprename  37808  dvdsrabdioph  37870  pell14qrdivcl  37925  monotoddzz  38003  jm2.19lem2  38052  jm2.19  38055  relexpaddss  38504  k0004lem3  38941  dvconstbi  39027  chordthmALT  39657  isosctrlem1ALT  39658  ssinc  39751  ssdec  39752  unima  39829  wessf1ornlem  39854  disjf1o  39861  disjinfi  39863  ssnnf1octb  39865  projf1o  39869  mapssbi  39886  iunmapsn  39890  fvelimad  39936  upbdrech  39994  iuneqfzuzlem  40024  suplesup  40029  rexabslelem  40118  climxrrelem  40455  limsupresxr  40472  liminfresxr  40473  liminfvalxr  40489  cncfshift  40561  cncfperiod  40566  cncfuni  40573  icccncfext  40574  dvmptfprodlem  40633  dvnprodlem1  40635  itgspltprt  40668  ismbl3  40676  stoweidlem3  40693  stoweidlem10  40700  stoweidlem19  40709  stoweidlem31  40721  stoweidlem34  40724  stoweidlem44  40734  fourierdlem41  40838  fourierdlem42  40839  fourierdlem51  40847  fourierdlem68  40864  fourierdlem89  40885  fourierdlem91  40887  fourierdlem92  40888  fourierdlem94  40890  etransclem24  40948  etransclem34  40958  rrxdsfi  40978  qndenserrnbllem  40987  salincl  41016  saldifcl2  41019  subsalsal  41050  sge0pr  41084  sge0pnffigt  41086  sge0reuz  41137  nnfoctbdjlem  41145  nnfoctbdj  41146  meadjiunlem  41155  caratheodorylem2  41217  hoidmv1le  41284  hoidmvlelem3  41287  hspmbllem2  41317  opnvonmbllem2  41323  sssmf  41423  smfaddlem1  41447  sigaraf  41518  sigarmf  41519  nltle2tri  41892  subsubelfzo0  41905  iccpartiltu  41927  icceuelpart  41941  pfxsuffeqwrdeq  41975  pfxsuff1eqwrdeq  41976  ccatpfx  41978  pfxpfx  41984  pfxccatin12lem1  41992  pfxccatpfx1  41996  pfxccatpfx2  41997  repswpfx  42005  pfxco  42007  proththd  42100  mogoldbblem  42198  bgoldbtbndlem2  42263  xpprsng  42672  nn0sumltlt  42690  invginvrid  42710  ply1sclrmsm  42733  linccl  42765  lincvalpr  42769  lincresunit3lem1  42830  lincresunit3  42832  fdivmpt  42896  nnolog2flm1  42946  dignnld  42959  digexp  42963  dignn0flhalflem1  42971  setrec2fun  43001  reccot  43064  rectan  43065