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  2632  eqeu  3661  onunel  6418  iotan0  6476  funopg  6520  dff1o2  6773  fvelimad  6895  unima  6903  fnimapr  6911  fvmptt  6955  fnreseql  6987  xpprsng  7079  f1elima  7203  f1ounsn  7212  f13dfv  7214  f1ocnvfvb  7219  f1cdmsn  7222  f1ofvswap  7246  oprssov  7521  resf1extb  7870  resf1ext2b  7871  funelss  7985  poxp  8064  poxp2  8079  poxp3  8086  smoiso  8288  oaord  8468  oaword  8470  omcan  8490  omwordri  8493  odi  8500  omeulem1  8503  oeord  8509  oecan  8510  oewordri  8513  oeordsuc  8515  nnaord  8540  nnaordr  8541  nndi  8544  nnaword  8548  nnmwordri  8557  naddel2  8609  naddss1  8610  naddss2  8611  erov  8744  ecopovtrn  8750  mapsnd  8816  f1dom3g  8896  xpdom3  8995  mapxpen  9063  dif1en  9078  findcard  9080  f1domfi2  9098  entrfir  9107  domtrfil  9108  domtrfir  9110  sbthfilem  9114  sdomdomtrfi  9117  php3  9125  findcard3  9174  indexfi  9251  suppr  9363  infpr  9396  r111  9675  tcrank  9784  acndom  9949  infdif2  10107  infxpdom  10108  cfeq0  10154  cfsuc  10155  cfflb  10157  cflim2  10161  cfsmolem  10168  axcc3  10336  domtriomlem  10340  axdc3lem2  10349  axdc3lem4  10351  axdc4lem  10353  axcclem  10355  pwcfsdom  10481  tsktrss  10659  tsksuc  10660  tskuni  10681  adderpqlem  10852  mulerpqlem  10853  mulcanenq  10858  distrnq  10859  ltsonq  10867  ltanq  10869  ltmnq  10870  distrlem1pr  10923  distrlem5pr  10925  ltsopr  10930  ltsosr  10992  ltasr  10998  adddir  11110  axlttrn  11192  letr  11214  nnncan1  11404  npncan3  11406  pnpcan2  11408  subdi  11557  subdir  11558  mulcan1g  11777  mulcan2g  11778  divmul  11786  div23  11802  div13  11804  muldivdir  11821  divsubdir  11822  subdivcomb1  11823  divcan7  11837  ltmul2  11979  lemul1  11980  lemul2  11981  lemul2a  11983  lediv1  11994  ltmuldiv2  12003  lemuldiv  12009  lemuldiv2  12010  ltdiv2  12015  lediv2  12019  infrelb  12114  nndivtr  12179  bndndx  12387  nn0n0n1ge2  12456  fnn0ind  12578  addlelt  13008  xrletr  13059  qsqueeze  13102  xleadd2a  13155  xleadd1  13156  xltadd2  13158  xltmul2  13194  supxrbnd  13229  iooneg  13373  iccneg  13374  icoshft  13375  icoshftf1o  13376  zltaddlt1le  13407  fzen  13443  uzsubsubfz  13448  ssfzunsnext  13471  fzrevral2  13515  fzshftral  13517  fz0fzdiffz0  13539  elfzmlbp  13541  elfzo  13563  nelfzo  13566  fzoaddel2  13622  fzosubel2  13627  ssfzo12bi  13663  fzonfzoufzol  13673  subfzo0  13694  flltdivnn0lt  13739  modmulnn  13795  modcyc  13812  modaddabs  13817  modaddmod  13818  modmuladd  13822  modadd2mod  13830  modsubmod  13838  modsubmodmod  13839  modaddmodup  13843  modmulmod  13845  modsubdir  13849  modfzo0difsn  13852  modsumfzodifsn  13853  uzindi  13891  axdc4uzlem  13892  expneg2  13979  expdiv  14022  expubnd  14087  mulbinom2  14132  bernneq2  14139  expnngt1  14150  hashinfxadd  14294  hashunsngx  14302  hashunsnggt  14303  hashfundm  14351  hashf1dmcdm  14353  hashdifsnp1  14415  ccatval3  14488  ccatfv0  14493  ccatval1lsw  14494  ccats1val2  14537  ccatw2s1p1  14546  swrdnd  14564  pfxsuffeqwrdeq  14607  pfxsuff1eqwrdeq  14608  swrdswrd  14614  pfxpfx  14617  wrd2ind  14632  swrdccatin1  14634  pfxccatin12lem1  14637  swrdccatin2  14638  pfxccatin12lem3  14641  swrdccat  14644  pfxccatpfx1  14645  pfxccatpfx2  14646  swrdccat3blem  14648  repswswrd  14693  repswpfx  14694  repswccat  14695  cshwidxmod  14712  2cshw  14722  3cshw  14727  scshwfzeqfzo  14735  cshwcsh2id  14737  cshimadifsn  14738  cshimadifsn0  14739  ccatco  14744  cshco  14745  swrdco  14746  pfxco  14747  lswco  14748  swrds2  14849  2swrd2eqwrdeq  14862  shftuz  14978  abs3dif  15241  fsumdifsnconst  15700  modfsummods  15702  sin02gt0  16103  dvdsval2  16168  dvdscmul  16195  dvdsmulc  16196  dvdscmulr  16197  dvdsmulcr  16198  divalglem8  16313  ndvdssub  16322  dvdsexpim  16468  rpmulgcd  16470  expgcd  16476  zexpgcd  16478  coprmprod  16574  cncongr1  16580  cncongr2  16581  isprm3  16596  modprm0  16719  coprimeprodsq  16722  pythagtriplem12  16740  pythagtriplem14  16742  pcprendvds  16754  pcmul  16765  pcdiv  16766  pcqcl  16770  pcqdiv  16771  pcdvdsb  16783  vdwnnlem1  16909  hashbcss  16918  cshwshashlem1  17009  fvsetsid  17081  setsstruct2  17087  setsstruct  17089  mrcss  17524  mrcsscl  17528  mrcun  17530  cofulid  17799  catcisolem  18019  funcsetcestrclem9  18071  latleeqj1  18359  lubun  18423  clatleglb  18426  pslem  18480  dirtr  18510  mgmb1mgm1  18565  pwspjmhm  18740  grpinvid1  18906  grpinvid2  18907  grpasscan1  18916  grpasscan2  18917  grpinvadd  18933  grpsubf  18934  grpsubrcan  18936  grpinvsub  18937  grpsubeq0  18941  grpsubadd0sub  18942  grppncan  18946  grpnpcan  18947  mulgnn0p1  19000  mulgaddcomlem  19012  mulginvcom  19014  mulginvinv  19015  subgsubcl  19052  subgsub  19053  eqglact  19093  qussub  19105  ghmsub  19138  psgnunilem4  19411  oddvds2  19480  odsubdvds  19485  gexnnod  19502  slwn0  19529  dvrcl  20324  unitdvcl  20325  dvrcan1  20329  dvrcan3  20330  dvreq1  20331  rngisom1  20386  rngisomring  20387  subrgdv  20506  abvsubtri  20744  idsrngd  20773  lmodvsubval2  20852  lsmcl  21019  lsmsp2  21023  lspsntrim  21034  rngqiprngimfolem  21229  lidldvgen  21273  cncrng  21327  chrcong  21466  dvdschrmulg  21467  zndvds  21488  zntoslem  21495  ocvsscon  21614  obselocv  21667  frlmphl  21720  ascldimul  21827  mpfsubrg  22039  ply1tmcl  22187  eqcoe1ply1eq  22215  gsummoncoe1  22224  lply1binomsc  22227  mamudm  22311  mamufacex  22312  scmatf1  22447  scmatf1o  22448  scmatrngiso  22452  submabas  22494  mdetdiaglem  22514  mdetralt2  22525  mdetero  22526  mdetunilem2  22529  mdetunilem6  22533  m2detleiblem7  22543  maducoeval2  22556  gsummatr01lem3  22573  gsummatr01  22575  smadiadetglem2  22588  cramerlem1  22603  mply1topmatcl  22721  mp2pm2mplem4  22725  ntrin  22977  elnei  23027  neindisj2  23039  ordtopn3  23112  leordtval2  23128  lecldbas  23135  cnrest2  23202  cmpsublem  23315  ptrescn  23555  xkococn  23576  kqfeq  23640  snfbas  23782  neifil  23796  fclsrest  23940  utopsnnei  24165  neipcfilu  24211  psmetsym  24226  psmetge0  24228  xmetge0  24260  xmetsym  24263  metustto  24469  metustbl  24482  restmetu  24486  nm2dif  24541  nmtri  24542  cnmet  24687  cnmpopc  24850  iihalf1  24853  iihalf2  24856  iocopnst  24865  clmnegsubdi2  25033  clmsub4  25034  clmvsubval2  25038  ncvspi  25084  cphsqrtcl3  25115  cph2ass  25141  cphipval2  25169  cphipval  25171  caublcls  25237  bcthlem3  25254  bcthlem4  25255  srabn  25288  cssbn  25303  cmslsschl  25305  rrxmet  25336  rrxdsfi  25339  iblconst  25747  dvdsq1p  26096  coeid3  26173  aannenlem2  26265  pserdvlem2  26366  tanord1  26474  cxpef  26602  recxpcl  26612  logbchbase  26709  relogbcl  26711  relogbzcl  26712  logbleb  26721  logblt  26722  relogbcxpb  26725  lawcos  26754  pythag  26755  isosctrlem1  26756  isosctrlem2  26757  lgsmodeq  27281  lgsmulsqcoprm  27282  gausslemma2dlem1a  27304  2lgsoddprmlem2  27348  sltres  27602  sletr  27698  cofcutr  27869  lrrecpo  27885  sltadd2im  27930  sleadd2im  27932  sleadd1  27933  sleadd2  27934  sltadd1  27936  addscan2  27937  addscan1  27938  sltsub1  28017  divsmulw  28133  zsoring  28333  ax5seglem1  28908  axcontlem2  28945  axcontlem8  28951  upgrpredgv  29119  numedglnl  29124  issubgr2  29252  uhgrissubgr  29255  egrsubgr  29257  nbusgrfi  29354  nb3grprlem2  29361  cplgr3v  29415  cusgrsizeindslem  29432  finsumvtxdg2size  29531  rusgrpropadjvtx  29566  upgrwlkvtxedg  29625  usgr2trlncl  29740  uspgrn2crct  29788  crctcshwlkn0lem4  29793  crctcshwlkn0lem5  29794  wwlksnextproplem3  29891  umgr2adedgwlklem  29924  rusgr0edg  29956  clwwlk1loop  29970  clwwlkccatlem  29971  clwlkclwwlklem2a4  29979  clwlkclwwlklem2a  29980  clwwisshclwwslemlem  29995  erclwwlktr  30004  clwwlkel  30028  erclwwlkntr  30053  clwwlknonex2lem2  30090  uhgr3cyclex  30164  umgr3cyclex  30165  eucrctshift  30225  frgr3v  30257  3cyclfrgrrn  30268  frgrwopreglem5a  30293  frgr2wsp1  30312  extwwlkfab  30334  clwwlknonclwlknonf1o  30344  numclwwlk3lem1  30364  numclwwlk5  30370  numclwwlk6  30372  isgrpo  30479  grpoinvid1  30510  grpoinvid2  30511  grpoinvop  30515  grpodivinv  30518  grpoinvdiv  30519  grpodivf  30520  grponpcan  30525  ablonncan  30538  nvmval  30624  nvmval2  30625  nvmfval  30626  nvmul0or  30632  nvpncan2  30635  nvaddsub4  30639  nvmeq0  30640  nvdif  30648  nvpi  30649  nvmtri  30653  nvabs  30654  imsmetlem  30672  ipval2lem3  30687  ipval2  30689  4ipval2  30690  ipval3  30691  nmooge0  30749  blometi  30785  hvaddsub12  31020  hvsubdistr1  31031  hvsubdistr2  31032  hvaddcan2  31053  hvmulcan  31054  hvmulcan2  31055  hvsubcan  31056  hvsubcan2  31057  his7  31072  his2sub  31074  his2sub2  31075  norm3dif2  31133  shsubcl  31202  hhssnv  31246  shlej2  31343  fh2  31601  cm2j  31602  pjoi0  31699  hodcl  31729  hosubdi  31790  unopf1o  31898  unopadj  31901  adj2  31916  braadd  31927  bramul  31928  lnopaddmuli  31955  lnopsubmuli  31957  homco2  31959  lnfnaddmuli  32027  adjlnop  32068  leopmul  32116  leoptr  32119  pjimai  32158  atcv1  32362  atexch  32363  atcvatlem  32367  fcoinvbr  32587  preiman0  32695  divnumden2  32803  sgn3da  32822  xdivmul  32912  cshf1o  32950  resvsca  33304  idlsrgcmnd  33487  hasheuni  34119  difelsiga  34167  cndprobin  34468  bayesth  34473  signstfvp  34605  breprexplemc  34666  trssfir1om  35143  trssfir1omregs  35153  fineqvac  35160  fineqvnttrclselem1  35162  fineqvnttrclselem3  35164  swrdrevpfx  35182  swrdwlk  35192  lediv2aALT  35742  fununiq  35834  dfrdg2  35858  clsun  36393  neiin  36397  rdgeqoa  37435  curfv  37661  matunitlindflem1  37677  poimirlem32  37713  ftc1anclem4  37757  areacirc  37774  filbcmb  37801  ismtybnd  37868  grpoeqdivid  37942  ghomco  37952  rngonegrmul  38005  zerdivemp1x  38008  rngohomco  38035  rngoisoco  38043  riscer  38049  intidl  38090  isfldidl  38129  eceldmqsxrncnvepres  38481  eceldmqsxrncnvepres2  38482  brredunds  38743  lshpnelb  39104  opnlen0  39308  opcon3b  39316  opcon2b  39317  oplecon3b  39320  opltcon3b  39324  opltcon2b  39326  oldmm1  39337  oldmm4  39340  oldmj1  39341  oldmj4  39344  cvrval2  39394  cvrcon3b  39397  leatb  39412  atcmp  39431  atcvreq0  39434  atlatle  39440  athgt  39576  3dim2  39588  islln2a  39637  lplnnleat  39662  lvolnleat  39703  4atlem10  39726  4atlem11  39729  4atlem12  39732  dalem21  39814  dalem22  39815  dalem23  39816  dalem29  39821  dalem30  39822  dalem31N  39823  dalem32  39824  dalem33  39825  dalem34  39826  dalem35  39827  dalem36  39828  dalem37  39829  dalem40  39832  dalem46  39838  dalem47  39839  dalem51  39843  dalem52  39844  dalem58  39850  dalem59  39851  pmaple  39881  paddclN  39962  pmapjoin  39972  pmapjat1  39973  elpcliN  40013  pclssN  40014  pclun2N  40019  2polcon4bN  40038  paddunN  40047  poldmj1N  40048  pmapj2N  40049  pmapocjN  40050  psubclinN  40068  paddatclN  40069  poml4N  40073  lautco  40217  ldilco  40236  ltrneq2  40268  trljat1  40286  cdlemc1  40311  cdleme10  40374  ltrnco  40839  trlcocnv  40840  trljco  40860  trljco2  40861  cdlemi1  40938  tendocnv  41141  diaord  41167  dibord  41279  dihord3  41377  dihord4  41378  dihmeetlem2N  41419  dihmeetlem4preN  41426  dochdmj1  41510  hdmap10lem  41959  lcmineqlem1  42143  sticksstones2  42261  readdsub  42503  reltsub1  42505  renpncan3  42510  reppncan  42512  resubdi  42515  readdcan2  42532  mzprename  42867  dvdsrabdioph  42928  pell14qrdivcl  42983  monotoddzz  43061  jm2.19lem2  43108  jm2.19  43111  relexpaddss  43836  k0004lem3  44267  dvconstbi  44452  chordthmALT  45050  isosctrlem1ALT  45051  ssinc  45209  ssdec  45210  wessf1ornlem  45307  disjf1o  45313  ssnnf1octb  45316  projf1o  45319  mapssbi  45335  iunmapsn  45339  upbdrech  45431  iuneqfzuzlem  45458  suplesup  45463  rexabslelem  45541  climxrrelem  45872  limsupresxr  45889  liminfresxr  45890  liminfvalxr  45906  xlimliminflimsup  45985  cncfshift  45997  cncfperiod  46002  cncfuni  46009  icccncfext  46010  dvmptfprodlem  46067  dvnprodlem1  46069  itgspltprt  46102  ismbl3  46109  stoweidlem3  46126  stoweidlem10  46133  stoweidlem19  46142  stoweidlem31  46154  stoweidlem34  46157  stoweidlem44  46167  fourierdlem41  46271  fourierdlem42  46272  fourierdlem51  46280  fourierdlem68  46297  fourierdlem89  46318  fourierdlem91  46320  fourierdlem92  46321  fourierdlem94  46323  etransclem24  46381  etransclem34  46391  qndenserrnbllem  46417  salincl  46447  saldifcl2  46451  subsalsal  46482  sge0pr  46517  sge0pnffigt  46519  sge0reuz  46570  nnfoctbdjlem  46578  nnfoctbdj  46579  meadjiunlem  46588  caratheodorylem2  46650  hoidmv1le  46717  hoidmvlelem3  46720  hspmbllem2  46750  opnvonmbllem2  46756  sssmf  46861  smfaddlem1  46886  sigaraf  46976  sigarmf  46977  nltle2tri  47438  subsubelfzo0  47451  submodaddmod  47466  zplusmodne  47468  addmodne  47469  minusmod5ne  47474  submodneaddmod  47476  modmkpkne  47486  modmknepk  47487  iccpartiltu  47547  icceuelpart  47561  poprelb  47649  reuopreuprim  47651  proththd  47739  mogoldbblem  47845  fppr2odd  47856  fpprel2  47866  bgoldbtbndlem2  47931  clnbusgrfi  47968  grimuhgr  48012  uhgrimisgrgric  48056  clnbgrgrim  48059  grtrif1o  48067  grlimgrtri  48128  gpgusgralem  48181  gpgedgvtx0  48186  gpgedg2ov  48191  gpgedg2iv  48192  gpg5nbgrvtx03starlem2  48194  nn0sumltlt  48475  invginvrid  48492  ply1sclrmsm  48509  linccl  48540  lincvalpr  48544  lincresunit3lem1  48605  lincresunit3  48607  fdivmpt  48666  nnolog2flm1  48716  dignnld  48729  digexp  48733  dignn0flhalflem1  48741  itcovalsucov  48794  reorelicc  48836  eenglngeehlnmlem1  48863  line2  48878  line2xlem  48879  itsclc0lem1  48882  itsclc0xyqsolr  48895  i0oii  49045  io1ii  49046  indthinc  49588  indthincALT  49589  setrec2fun  49818  reccot  49884  rectan  49885