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  2630  vtoclegftOLD  3544  eqeu  3665  onunel  6413  iotan0  6471  funopg  6515  dff1o2  6768  fvelimad  6889  unima  6897  fnimapr  6905  fvmptt  6949  fnreseql  6981  xpprsng  7073  f1elima  7197  f1ounsn  7206  f13dfv  7208  f1ocnvfvb  7213  f1cdmsn  7216  f1ofvswap  7240  oprssov  7515  resf1extb  7864  resf1ext2b  7865  funelss  7979  poxp  8058  poxp2  8073  poxp3  8080  smoiso  8282  oaord  8462  oaword  8464  omcan  8484  omwordri  8487  odi  8494  omeulem1  8497  oeord  8503  oecan  8504  oewordri  8507  oeordsuc  8509  nnaord  8534  nnaordr  8535  nndi  8538  nnaword  8542  nnmwordri  8551  naddel2  8603  naddss1  8604  naddss2  8605  erov  8738  ecopovtrn  8744  mapsnd  8810  f1dom3g  8890  xpdom3  8988  mapxpen  9056  dif1en  9071  findcard  9073  f1domfi2  9091  entrfir  9100  domtrfil  9101  domtrfir  9103  sbthfilem  9107  sdomdomtrfi  9110  php3  9118  findcard3  9167  indexfi  9244  suppr  9356  infpr  9389  r111  9668  tcrank  9777  acndom  9942  infdif2  10100  infxpdom  10101  cfeq0  10147  cfsuc  10148  cfflb  10150  cflim2  10154  cfsmolem  10161  axcc3  10329  domtriomlem  10333  axdc3lem2  10342  axdc3lem4  10344  axdc4lem  10346  axcclem  10348  pwcfsdom  10474  tsktrss  10652  tsksuc  10653  tskuni  10674  adderpqlem  10845  mulerpqlem  10846  mulcanenq  10851  distrnq  10852  ltsonq  10860  ltanq  10862  ltmnq  10863  distrlem1pr  10916  distrlem5pr  10918  ltsopr  10923  ltsosr  10985  ltasr  10991  adddir  11103  axlttrn  11185  letr  11207  nnncan1  11397  npncan3  11399  pnpcan2  11401  subdi  11550  subdir  11551  mulcan1g  11770  mulcan2g  11771  divmul  11779  div23  11795  div13  11797  muldivdir  11814  divsubdir  11815  subdivcomb1  11816  divcan7  11830  ltmul2  11972  lemul1  11973  lemul2  11974  lemul2a  11976  lediv1  11987  ltmuldiv2  11996  lemuldiv  12002  lemuldiv2  12003  ltdiv2  12008  lediv2  12012  infrelb  12107  nndivtr  12172  bndndx  12380  nn0n0n1ge2  12449  fnn0ind  12572  addlelt  13006  xrletr  13057  qsqueeze  13100  xleadd2a  13153  xleadd1  13154  xltadd2  13156  xltmul2  13192  supxrbnd  13227  iooneg  13371  iccneg  13372  icoshft  13373  icoshftf1o  13374  zltaddlt1le  13405  fzen  13441  uzsubsubfz  13446  ssfzunsnext  13469  fzrevral2  13513  fzshftral  13515  fz0fzdiffz0  13537  elfzmlbp  13539  elfzo  13561  nelfzo  13564  fzoaddel2  13620  fzosubel2  13625  ssfzo12bi  13661  fzonfzoufzol  13671  subfzo0  13692  flltdivnn0lt  13737  modmulnn  13793  modcyc  13810  modaddabs  13815  modaddmod  13816  modmuladd  13820  modadd2mod  13828  modsubmod  13836  modsubmodmod  13837  modaddmodup  13841  modmulmod  13843  modsubdir  13847  modfzo0difsn  13850  modsumfzodifsn  13851  uzindi  13889  axdc4uzlem  13890  expneg2  13977  expdiv  14020  expubnd  14085  mulbinom2  14130  bernneq2  14137  expnngt1  14148  hashinfxadd  14292  hashunsngx  14300  hashunsnggt  14301  hashfundm  14349  hashf1dmcdm  14351  hashdifsnp1  14413  ccatval3  14486  ccatfv0  14491  ccatval1lsw  14492  ccats1val2  14535  ccatw2s1p1  14544  swrdnd  14562  pfxsuffeqwrdeq  14605  pfxsuff1eqwrdeq  14606  swrdswrd  14612  pfxpfx  14615  wrd2ind  14630  swrdccatin1  14632  pfxccatin12lem1  14635  swrdccatin2  14636  pfxccatin12lem3  14639  swrdccat  14642  pfxccatpfx1  14643  pfxccatpfx2  14644  swrdccat3blem  14646  repswswrd  14691  repswpfx  14692  repswccat  14693  cshwidxmod  14710  2cshw  14720  3cshw  14725  scshwfzeqfzo  14733  cshwcsh2id  14735  cshimadifsn  14736  cshimadifsn0  14737  ccatco  14742  cshco  14743  swrdco  14744  pfxco  14745  lswco  14746  swrds2  14847  2swrd2eqwrdeq  14860  shftuz  14976  abs3dif  15239  fsumdifsnconst  15698  modfsummods  15700  sin02gt0  16101  dvdsval2  16166  dvdscmul  16193  dvdsmulc  16194  dvdscmulr  16195  dvdsmulcr  16196  divalglem8  16311  ndvdssub  16320  dvdsexpim  16466  rpmulgcd  16468  expgcd  16474  zexpgcd  16476  coprmprod  16572  cncongr1  16578  cncongr2  16579  isprm3  16594  modprm0  16717  coprimeprodsq  16720  pythagtriplem12  16738  pythagtriplem14  16740  pcprendvds  16752  pcmul  16763  pcdiv  16764  pcqcl  16768  pcqdiv  16769  pcdvdsb  16781  vdwnnlem1  16907  hashbcss  16916  cshwshashlem1  17007  fvsetsid  17079  setsstruct2  17085  setsstruct  17087  mrcss  17522  mrcsscl  17526  mrcun  17528  cofulid  17797  catcisolem  18017  funcsetcestrclem9  18069  latleeqj1  18357  lubun  18421  clatleglb  18424  pslem  18478  dirtr  18508  mgmb1mgm1  18563  pwspjmhm  18738  grpinvid1  18904  grpinvid2  18905  grpasscan1  18914  grpasscan2  18915  grpinvadd  18931  grpsubf  18932  grpsubrcan  18934  grpinvsub  18935  grpsubeq0  18939  grpsubadd0sub  18940  grppncan  18944  grpnpcan  18945  mulgnn0p1  18998  mulgaddcomlem  19010  mulginvcom  19012  mulginvinv  19013  subgsubcl  19050  subgsub  19051  eqglact  19092  qussub  19104  ghmsub  19137  psgnunilem4  19410  oddvds2  19479  odsubdvds  19484  gexnnod  19501  slwn0  19528  dvrcl  20323  unitdvcl  20324  dvrcan1  20328  dvrcan3  20329  dvreq1  20330  rngisom1  20385  rngisomring  20386  subrgdv  20505  abvsubtri  20743  idsrngd  20772  lmodvsubval2  20851  lsmcl  21018  lsmsp2  21022  lspsntrim  21033  rngqiprngimfolem  21228  lidldvgen  21272  cncrng  21326  chrcong  21465  dvdschrmulg  21466  zndvds  21487  zntoslem  21494  ocvsscon  21613  obselocv  21666  frlmphl  21719  ascldimul  21826  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  28907  axcontlem2  28944  axcontlem8  28950  upgrpredgv  29118  numedglnl  29123  issubgr2  29251  uhgrissubgr  29254  egrsubgr  29256  nbusgrfi  29353  nb3grprlem2  29360  cplgr3v  29414  cusgrsizeindslem  29431  finsumvtxdg2size  29530  rusgrpropadjvtx  29565  upgrwlkvtxedg  29624  usgr2trlncl  29739  uspgrn2crct  29787  crctcshwlkn0lem4  29792  crctcshwlkn0lem5  29793  wwlksnextproplem3  29890  umgr2adedgwlklem  29923  rusgr0edg  29952  clwwlk1loop  29966  clwwlkccatlem  29967  clwlkclwwlklem2a4  29975  clwlkclwwlklem2a  29976  clwwisshclwwslemlem  29991  erclwwlktr  30000  clwwlkel  30024  erclwwlkntr  30049  clwwlknonex2lem2  30086  uhgr3cyclex  30160  umgr3cyclex  30161  eucrctshift  30221  frgr3v  30253  3cyclfrgrrn  30264  frgrwopreglem5a  30289  frgr2wsp1  30308  extwwlkfab  30330  clwwlknonclwlknonf1o  30340  numclwwlk3lem1  30360  numclwwlk5  30366  numclwwlk6  30368  isgrpo  30475  grpoinvid1  30506  grpoinvid2  30507  grpoinvop  30511  grpodivinv  30514  grpoinvdiv  30515  grpodivf  30516  grponpcan  30521  ablonncan  30534  nvmval  30620  nvmval2  30621  nvmfval  30622  nvmul0or  30628  nvpncan2  30631  nvaddsub4  30635  nvmeq0  30636  nvdif  30644  nvpi  30645  nvmtri  30649  nvabs  30650  imsmetlem  30668  ipval2lem3  30683  ipval2  30685  4ipval2  30686  ipval3  30687  nmooge0  30745  blometi  30781  hvaddsub12  31016  hvsubdistr1  31027  hvsubdistr2  31028  hvaddcan2  31049  hvmulcan  31050  hvmulcan2  31051  hvsubcan  31052  hvsubcan2  31053  his7  31068  his2sub  31070  his2sub2  31071  norm3dif2  31129  shsubcl  31198  hhssnv  31242  shlej2  31339  fh2  31597  cm2j  31598  pjoi0  31695  hodcl  31725  hosubdi  31786  unopf1o  31894  unopadj  31897  adj2  31912  braadd  31923  bramul  31924  lnopaddmuli  31951  lnopsubmuli  31953  homco2  31955  lnfnaddmuli  32023  adjlnop  32064  leopmul  32112  leoptr  32115  pjimai  32154  atcv1  32358  atexch  32359  atcvatlem  32363  fcoinvbr  32583  preiman0  32689  divnumden2  32796  sgn3da  32815  xdivmul  32903  cshf1o  32941  resvsca  33295  idlsrgcmnd  33478  hasheuni  34096  difelsiga  34144  cndprobin  34445  bayesth  34450  signstfvp  34582  breprexplemc  34643  trssfir1om  35120  trssfir1omregs  35130  fineqvac  35137  fineqvnttrclselem1  35139  fineqvnttrclselem3  35141  swrdrevpfx  35159  swrdwlk  35169  lediv2aALT  35719  fununiq  35811  dfrdg2  35835  clsun  36368  neiin  36372  rdgeqoa  37410  curfv  37646  matunitlindflem1  37662  poimirlem32  37698  ftc1anclem4  37742  areacirc  37759  filbcmb  37786  ismtybnd  37853  grpoeqdivid  37927  ghomco  37937  rngonegrmul  37990  zerdivemp1x  37993  rngohomco  38020  rngoisoco  38028  riscer  38034  intidl  38075  isfldidl  38114  eceldmqsxrncnvepres  38450  eceldmqsxrncnvepres2  38451  brredunds  38669  lshpnelb  39029  opnlen0  39233  opcon3b  39241  opcon2b  39242  oplecon3b  39245  opltcon3b  39249  opltcon2b  39251  oldmm1  39262  oldmm4  39265  oldmj1  39266  oldmj4  39269  cvrval2  39319  cvrcon3b  39322  leatb  39337  atcmp  39356  atcvreq0  39359  atlatle  39365  athgt  39501  3dim2  39513  islln2a  39562  lplnnleat  39587  lvolnleat  39628  4atlem10  39651  4atlem11  39654  4atlem12  39657  dalem21  39739  dalem22  39740  dalem23  39741  dalem29  39746  dalem30  39747  dalem31N  39748  dalem32  39749  dalem33  39750  dalem34  39751  dalem35  39752  dalem36  39753  dalem37  39754  dalem40  39757  dalem46  39763  dalem47  39764  dalem51  39768  dalem52  39769  dalem58  39775  dalem59  39776  pmaple  39806  paddclN  39887  pmapjoin  39897  pmapjat1  39898  elpcliN  39938  pclssN  39939  pclun2N  39944  2polcon4bN  39963  paddunN  39972  poldmj1N  39973  pmapj2N  39974  pmapocjN  39975  psubclinN  39993  paddatclN  39994  poml4N  39998  lautco  40142  ldilco  40161  ltrneq2  40193  trljat1  40211  cdlemc1  40236  cdleme10  40299  ltrnco  40764  trlcocnv  40765  trljco  40785  trljco2  40786  cdlemi1  40863  tendocnv  41066  diaord  41092  dibord  41204  dihord3  41302  dihord4  41303  dihmeetlem2N  41344  dihmeetlem4preN  41351  dochdmj1  41435  hdmap10lem  41884  lcmineqlem1  42068  sticksstones2  42186  readdsub  42423  reltsub1  42425  renpncan3  42430  reppncan  42432  resubdi  42435  readdcan2  42452  mzprename  42788  dvdsrabdioph  42849  pell14qrdivcl  42904  monotoddzz  42982  jm2.19lem2  43029  jm2.19  43032  relexpaddss  43757  k0004lem3  44188  dvconstbi  44373  chordthmALT  44971  isosctrlem1ALT  44972  ssinc  45130  ssdec  45131  wessf1ornlem  45228  disjf1o  45234  ssnnf1octb  45237  projf1o  45240  mapssbi  45256  iunmapsn  45260  upbdrech  45352  iuneqfzuzlem  45379  suplesup  45384  rexabslelem  45462  climxrrelem  45793  limsupresxr  45810  liminfresxr  45811  liminfvalxr  45827  xlimliminflimsup  45906  cncfshift  45918  cncfperiod  45923  cncfuni  45930  icccncfext  45931  dvmptfprodlem  45988  dvnprodlem1  45990  itgspltprt  46023  ismbl3  46030  stoweidlem3  46047  stoweidlem10  46054  stoweidlem19  46063  stoweidlem31  46075  stoweidlem34  46078  stoweidlem44  46088  fourierdlem41  46192  fourierdlem42  46193  fourierdlem51  46201  fourierdlem68  46218  fourierdlem89  46239  fourierdlem91  46241  fourierdlem92  46242  fourierdlem94  46244  etransclem24  46302  etransclem34  46312  qndenserrnbllem  46338  salincl  46368  saldifcl2  46372  subsalsal  46403  sge0pr  46438  sge0pnffigt  46440  sge0reuz  46491  nnfoctbdjlem  46499  nnfoctbdj  46500  meadjiunlem  46509  caratheodorylem2  46571  hoidmv1le  46638  hoidmvlelem3  46641  hspmbllem2  46671  opnvonmbllem2  46677  sssmf  46782  smfaddlem1  46807  sigaraf  46897  sigarmf  46898  nltle2tri  47350  subsubelfzo0  47363  submodaddmod  47378  zplusmodne  47380  addmodne  47381  minusmod5ne  47386  submodneaddmod  47388  modmkpkne  47398  modmknepk  47399  iccpartiltu  47459  icceuelpart  47473  poprelb  47561  reuopreuprim  47563  proththd  47651  mogoldbblem  47757  fppr2odd  47768  fpprel2  47778  bgoldbtbndlem2  47843  clnbusgrfi  47880  grimuhgr  47924  uhgrimisgrgric  47968  clnbgrgrim  47971  grtrif1o  47979  grlimgrtri  48040  gpgusgralem  48093  gpgedgvtx0  48098  gpgedg2ov  48103  gpgedg2iv  48104  gpg5nbgrvtx03starlem2  48106  nn0sumltlt  48387  invginvrid  48404  ply1sclrmsm  48421  linccl  48452  lincvalpr  48456  lincresunit3lem1  48517  lincresunit3  48519  fdivmpt  48578  nnolog2flm1  48628  dignnld  48641  digexp  48645  dignn0flhalflem1  48653  itcovalsucov  48706  reorelicc  48748  eenglngeehlnmlem1  48775  line2  48790  line2xlem  48791  itsclc0lem1  48794  itsclc0xyqsolr  48807  i0oii  48957  io1ii  48958  indthinc  49500  indthincALT  49501  setrec2fun  49730  reccot  49796  rectan  49797