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

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

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 1089

This theorem is referenced by:  3ad2ant1  1134  3simpb  1150  3imp3i2an  1346  eupickb  2635  vtoclegftOLD  3589  eqeu  3712  onunel  6489  iotan0  6551  funopg  6600  dff1o2  6853  fvelimad  6976  unima  6984  fnimapr  6992  fvmptt  7036  fnreseql  7068  xpprsng  7160  f1elima  7283  f1ounsn  7292  f13dfv  7294  f1ocnvfvb  7299  f1cdmsn  7302  f1ofvswap  7326  oprssov  7602  resf1extb  7956  resf1ext2b  7957  funelss  8072  poxp  8153  poxp2  8168  poxp3  8175  wfrlem4OLD  8352  smoiso  8402  oaord  8585  oaword  8587  omcan  8607  omwordri  8610  odi  8617  omeulem1  8620  oeord  8626  oecan  8627  oewordri  8630  oeordsuc  8632  nnaord  8657  nnaordr  8658  nndi  8661  nnaword  8665  nnmwordri  8674  naddel2  8726  naddss1  8727  naddss2  8728  erov  8854  ecopovtrn  8860  mapsnd  8926  f1dom3g  9008  xpdom3  9110  mapxpen  9183  dif1en  9200  dif1enOLD  9202  findcard  9203  f1domfi2  9222  entrfir  9231  domtrfil  9232  domtrfir  9234  sbthfilem  9238  sdomdomtrfi  9241  php3  9249  findcard3  9318  indexfi  9400  suppr  9511  infpr  9543  r111  9815  tcrank  9924  acndom  10091  infdif2  10249  infxpdom  10250  cfeq0  10296  cfsuc  10297  cfflb  10299  cflim2  10303  cfsmolem  10310  axcc3  10478  domtriomlem  10482  axdc3lem2  10491  axdc3lem4  10493  axdc4lem  10495  axcclem  10497  pwcfsdom  10623  tsktrss  10801  tsksuc  10802  tskuni  10823  adderpqlem  10994  mulerpqlem  10995  mulcanenq  11000  distrnq  11001  ltsonq  11009  ltanq  11011  ltmnq  11012  distrlem1pr  11065  distrlem5pr  11067  ltsopr  11072  ltsosr  11134  ltasr  11140  adddir  11252  axlttrn  11333  letr  11355  nnncan1  11545  npncan3  11547  pnpcan2  11549  subdi  11696  subdir  11697  mulcan1g  11916  mulcan2g  11917  divmul  11925  div23  11941  div13  11943  muldivdir  11960  divsubdir  11961  subdivcomb1  11962  divcan7  11976  ltmul2  12118  lemul1  12119  lemul2  12120  lemul2a  12122  lediv1  12133  ltmuldiv2  12142  lemuldiv  12148  lemuldiv2  12149  ltdiv2  12154  lediv2  12158  infrelb  12253  nndivtr  12313  bndndx  12525  nn0n0n1ge2  12594  fnn0ind  12717  addlelt  13149  xrletr  13200  qsqueeze  13243  xleadd2a  13296  xleadd1  13297  xltadd2  13299  xltmul2  13335  supxrbnd  13370  iooneg  13511  iccneg  13512  icoshft  13513  icoshftf1o  13514  zltaddlt1le  13545  fzen  13581  uzsubsubfz  13586  ssfzunsnext  13609  fzrevral2  13653  fzshftral  13655  fz0fzdiffz0  13677  elfzmlbp  13679  elfzo  13701  nelfzo  13704  fzoaddel2  13759  fzosubel2  13764  ssfzo12bi  13800  fzonfzoufzol  13809  subfzo0  13828  flltdivnn0lt  13873  modmulnn  13929  modcyc  13946  modaddabs  13949  modaddmod  13950  modmuladd  13954  modadd2mod  13962  modsubmod  13970  modsubmodmod  13971  modaddmodup  13975  modmulmod  13977  modsubdir  13981  modfzo0difsn  13984  modsumfzodifsn  13985  uzindi  14023  axdc4uzlem  14024  expneg2  14111  expdiv  14154  expubnd  14217  mulbinom2  14262  bernneq2  14269  expnngt1  14280  hashinfxadd  14424  hashunsngx  14432  hashunsnggt  14433  hashfundm  14481  hashf1dmcdm  14483  hashdifsnp1  14545  ccatval3  14617  ccatfv0  14621  ccatval1lsw  14622  ccats1val2  14665  ccatw2s1p1  14674  swrdnd  14692  pfxsuffeqwrdeq  14736  pfxsuff1eqwrdeq  14737  swrdswrd  14743  pfxpfx  14746  wrd2ind  14761  swrdccatin1  14763  pfxccatin12lem1  14766  swrdccatin2  14767  pfxccatin12lem3  14770  swrdccat  14773  pfxccatpfx1  14774  pfxccatpfx2  14775  swrdccat3blem  14777  repswswrd  14822  repswpfx  14823  repswccat  14824  cshwidxmod  14841  2cshw  14851  3cshw  14856  scshwfzeqfzo  14865  cshwcsh2id  14867  cshimadifsn  14868  cshimadifsn0  14869  ccatco  14874  cshco  14875  swrdco  14876  pfxco  14877  lswco  14878  swrds2  14979  2swrd2eqwrdeq  14992  shftuz  15108  abs3dif  15370  fsumdifsnconst  15827  modfsummods  15829  sin02gt0  16228  dvdsval2  16293  dvdscmul  16320  dvdsmulc  16321  dvdscmulr  16322  dvdsmulcr  16323  divalglem8  16437  ndvdssub  16446  dvdsexpim  16592  rpmulgcd  16594  expgcd  16600  zexpgcd  16602  coprmprod  16698  cncongr1  16704  cncongr2  16705  isprm3  16720  modprm0  16843  coprimeprodsq  16846  pythagtriplem12  16864  pythagtriplem14  16866  pcprendvds  16878  pcmul  16889  pcdiv  16890  pcqcl  16894  pcqdiv  16895  pcdvdsb  16907  vdwnnlem1  17033  hashbcss  17042  cshwshashlem1  17133  fvsetsid  17205  setsstruct2  17211  setsstruct  17213  mrcss  17659  mrcsscl  17663  mrcun  17665  cofulid  17935  catcisolem  18155  funcsetcestrclem9  18208  latleeqj1  18496  lubun  18560  clatleglb  18563  pslem  18617  dirtr  18647  mgmb1mgm1  18668  pwspjmhm  18843  grpinvid1  19009  grpinvid2  19010  grpasscan1  19019  grpasscan2  19020  grpinvadd  19036  grpsubf  19037  grpsubrcan  19039  grpinvsub  19040  grpsubeq0  19044  grpsubadd0sub  19045  grppncan  19049  grpnpcan  19050  mulgnn0p1  19103  mulgaddcomlem  19115  mulginvcom  19117  mulginvinv  19118  subgsubcl  19155  subgsub  19156  eqglact  19197  qussub  19209  ghmsub  19242  psgnunilem4  19515  oddvds2  19584  odsubdvds  19589  gexnnod  19606  slwn0  19633  dvrcl  20404  unitdvcl  20405  dvrcan1  20409  dvrcan3  20410  dvreq1  20411  rngisom1  20466  rngisomring  20467  subrgdv  20589  abvsubtri  20828  idsrngd  20857  lmodvsubval2  20915  lsmcl  21082  lsmsp2  21086  lspsntrim  21097  rngqiprngimfolem  21300  lidldvgen  21344  cncrng  21401  chrcong  21542  dvdschrmulg  21543  zndvds  21568  zntoslem  21575  ocvsscon  21693  obselocv  21748  frlmphl  21801  ascldimul  21908  mpfsubrg  22127  ply1tmcl  22275  eqcoe1ply1eq  22303  gsummoncoe1  22312  lply1binomsc  22315  mamudm  22399  mamufacex  22400  scmatf1  22537  scmatf1o  22538  scmatrngiso  22542  submabas  22584  mdetdiaglem  22604  mdetralt2  22615  mdetero  22616  mdetunilem2  22619  mdetunilem6  22623  m2detleiblem7  22633  maducoeval2  22646  gsummatr01lem3  22663  gsummatr01  22665  smadiadetglem2  22678  cramerlem1  22693  mply1topmatcl  22811  mp2pm2mplem4  22815  ntrin  23069  elnei  23119  neindisj2  23131  ordtopn3  23204  leordtval2  23220  lecldbas  23227  cnrest2  23294  cmpsublem  23407  ptrescn  23647  xkococn  23668  kqfeq  23732  snfbas  23874  neifil  23888  fclsrest  24032  utopsnnei  24258  neipcfilu  24305  psmetsym  24320  psmetge0  24322  xmetge0  24354  xmetsym  24357  metustto  24566  metustbl  24579  restmetu  24583  nm2dif  24638  nmtri  24639  cnmet  24792  cnmpopc  24955  iihalf1  24958  iihalf2  24961  iocopnst  24970  clmnegsubdi2  25138  clmsub4  25139  clmvsubval2  25143  ncvspi  25190  cphsqrtcl3  25221  cph2ass  25247  cphipval2  25275  cphipval  25277  caublcls  25343  bcthlem3  25360  bcthlem4  25361  srabn  25394  cssbn  25409  cmslsschl  25411  rrxmet  25442  rrxdsfi  25445  iblconst  25853  dvdsq1p  26202  coeid3  26279  aannenlem2  26371  pserdvlem2  26472  tanord1  26579  cxpef  26707  recxpcl  26717  logbchbase  26814  relogbcl  26816  relogbzcl  26817  logbleb  26826  logblt  26827  relogbcxpb  26830  lawcos  26859  pythag  26860  isosctrlem1  26861  isosctrlem2  26862  lgsmodeq  27386  lgsmulsqcoprm  27387  gausslemma2dlem1a  27409  2lgsoddprmlem2  27453  sltres  27707  sletr  27803  cofcutr  27958  lrrecpo  27974  sltadd2im  28019  sleadd2im  28021  sleadd1  28022  sleadd2  28023  sltadd1  28025  addscan2  28026  addscan1  28027  sltsub1  28106  divsmulw  28218  ax5seglem1  28943  axcontlem2  28980  axcontlem8  28986  upgrpredgv  29156  numedglnl  29161  issubgr2  29289  uhgrissubgr  29292  egrsubgr  29294  nbusgrfi  29391  nb3grprlem2  29398  cplgr3v  29452  cusgrsizeindslem  29469  finsumvtxdg2size  29568  rusgrpropadjvtx  29603  upgrwlkvtxedg  29663  usgr2trlncl  29780  uspgrn2crct  29828  crctcshwlkn0lem4  29833  crctcshwlkn0lem5  29834  wwlksnextproplem3  29931  umgr2adedgwlklem  29964  rusgr0edg  29993  clwwlk1loop  30007  clwwlkccatlem  30008  clwlkclwwlklem2a4  30016  clwlkclwwlklem2a  30017  clwwisshclwwslemlem  30032  erclwwlktr  30041  clwwlkel  30065  erclwwlkntr  30090  clwwlknonex2lem2  30127  uhgr3cyclex  30201  umgr3cyclex  30202  eucrctshift  30262  frgr3v  30294  3cyclfrgrrn  30305  frgrwopreglem5a  30330  frgr2wsp1  30349  extwwlkfab  30371  clwwlknonclwlknonf1o  30381  numclwwlk3lem1  30401  numclwwlk5  30407  numclwwlk6  30409  isgrpo  30516  grpoinvid1  30547  grpoinvid2  30548  grpoinvop  30552  grpodivinv  30555  grpoinvdiv  30556  grpodivf  30557  grponpcan  30562  ablonncan  30575  nvmval  30661  nvmval2  30662  nvmfval  30663  nvmul0or  30669  nvpncan2  30672  nvaddsub4  30676  nvmeq0  30677  nvdif  30685  nvpi  30686  nvmtri  30690  nvabs  30691  imsmetlem  30709  ipval2lem3  30724  ipval2  30726  4ipval2  30727  ipval3  30728  nmooge0  30786  blometi  30822  hvaddsub12  31057  hvsubdistr1  31068  hvsubdistr2  31069  hvaddcan2  31090  hvmulcan  31091  hvmulcan2  31092  hvsubcan  31093  hvsubcan2  31094  his7  31109  his2sub  31111  his2sub2  31112  norm3dif2  31170  shsubcl  31239  hhssnv  31283  shlej2  31380  fh2  31638  cm2j  31639  pjoi0  31736  hodcl  31766  hosubdi  31827  unopf1o  31935  unopadj  31938  adj2  31953  braadd  31964  bramul  31965  lnopaddmuli  31992  lnopsubmuli  31994  homco2  31996  lnfnaddmuli  32064  adjlnop  32105  leopmul  32153  leoptr  32156  pjimai  32195  atcv1  32399  atexch  32400  atcvatlem  32404  fcoinvbr  32618  preiman0  32719  divnumden2  32817  xdivmul  32907  cshf1o  32947  resvsca  33356  idlsrgcmnd  33543  hasheuni  34086  difelsiga  34134  cndprobin  34436  bayesth  34441  sgn3da  34544  signstfvp  34586  breprexplemc  34647  fineqvac  35111  swrdrevpfx  35122  swrdwlk  35132  lediv2aALT  35682  fununiq  35769  dfrdg2  35796  clsun  36329  neiin  36333  rdgeqoa  37371  curfv  37607  matunitlindflem1  37623  poimirlem32  37659  ftc1anclem4  37703  areacirc  37720  filbcmb  37747  ismtybnd  37814  grpoeqdivid  37888  ghomco  37898  rngonegrmul  37951  zerdivemp1x  37954  rngohomco  37981  rngoisoco  37989  riscer  37995  intidl  38036  isfldidl  38075  brredunds  38627  lshpnelb  38985  opnlen0  39189  opcon3b  39197  opcon2b  39198  oplecon3b  39201  opltcon3b  39205  opltcon2b  39207  oldmm1  39218  oldmm4  39221  oldmj1  39222  oldmj4  39225  cvrval2  39275  cvrcon3b  39278  leatb  39293  atcmp  39312  atcvreq0  39315  atlatle  39321  athgt  39458  3dim2  39470  islln2a  39519  lplnnleat  39544  lvolnleat  39585  4atlem10  39608  4atlem11  39611  4atlem12  39614  dalem21  39696  dalem22  39697  dalem23  39698  dalem29  39703  dalem30  39704  dalem31N  39705  dalem32  39706  dalem33  39707  dalem34  39708  dalem35  39709  dalem36  39710  dalem37  39711  dalem40  39714  dalem46  39720  dalem47  39721  dalem51  39725  dalem52  39726  dalem58  39732  dalem59  39733  pmaple  39763  paddclN  39844  pmapjoin  39854  pmapjat1  39855  elpcliN  39895  pclssN  39896  pclun2N  39901  2polcon4bN  39920  paddunN  39929  poldmj1N  39930  pmapj2N  39931  pmapocjN  39932  psubclinN  39950  paddatclN  39951  poml4N  39955  lautco  40099  ldilco  40118  ltrneq2  40150  trljat1  40168  cdlemc1  40193  cdleme10  40256  ltrnco  40721  trlcocnv  40722  trljco  40742  trljco2  40743  cdlemi1  40820  tendocnv  41023  diaord  41049  dibord  41161  dihord3  41259  dihord4  41260  dihmeetlem2N  41301  dihmeetlem4preN  41308  dochdmj1  41392  hdmap10lem  41841  lcmineqlem1  42030  sticksstones2  42148  metakunt29  42234  metakunt30  42235  factwoffsmonot  42243  readdsub  42414  reltsub1  42416  renpncan3  42421  reppncan  42423  resubdi  42426  readdcan2  42442  mzprename  42760  dvdsrabdioph  42821  pell14qrdivcl  42876  monotoddzz  42955  jm2.19lem2  43002  jm2.19  43005  relexpaddss  43731  k0004lem3  44162  dvconstbi  44353  chordthmALT  44953  isosctrlem1ALT  44954  ssinc  45092  ssdec  45093  wessf1ornlem  45190  disjf1o  45196  ssnnf1octb  45199  projf1o  45202  mapssbi  45218  iunmapsn  45222  upbdrech  45317  iuneqfzuzlem  45345  suplesup  45350  rexabslelem  45429  climxrrelem  45764  limsupresxr  45781  liminfresxr  45782  liminfvalxr  45798  xlimliminflimsup  45877  cncfshift  45889  cncfperiod  45894  cncfuni  45901  icccncfext  45902  dvmptfprodlem  45959  dvnprodlem1  45961  itgspltprt  45994  ismbl3  46001  stoweidlem3  46018  stoweidlem10  46025  stoweidlem19  46034  stoweidlem31  46046  stoweidlem34  46049  stoweidlem44  46059  fourierdlem41  46163  fourierdlem42  46164  fourierdlem51  46172  fourierdlem68  46189  fourierdlem89  46210  fourierdlem91  46212  fourierdlem92  46213  fourierdlem94  46215  etransclem24  46273  etransclem34  46283  qndenserrnbllem  46309  salincl  46339  saldifcl2  46343  subsalsal  46374  sge0pr  46409  sge0pnffigt  46411  sge0reuz  46462  nnfoctbdjlem  46470  nnfoctbdj  46471  meadjiunlem  46480  caratheodorylem2  46542  hoidmv1le  46609  hoidmvlelem3  46612  hspmbllem2  46642  opnvonmbllem2  46648  sssmf  46753  smfaddlem1  46778  sigaraf  46868  sigarmf  46869  nltle2tri  47325  subsubelfzo0  47338  submodaddmod  47343  zplusmodne  47345  addmodne  47346  minusmod5ne  47351  submodneaddmod  47353  iccpartiltu  47409  icceuelpart  47423  poprelb  47511  reuopreuprim  47513  proththd  47601  mogoldbblem  47707  fppr2odd  47718  fpprel2  47728  bgoldbtbndlem2  47793  clnbusgrfi  47829  grimuhgr  47878  uhgrimisgrgric  47899  clnbgrgrim  47902  grtrif1o  47909  grlimgrtri  47963  gpgusgralem  48011  gpgedgvtx0  48019  gpg5nbgrvtx03starlem2  48025  nn0sumltlt  48266  invginvrid  48283  ply1sclrmsm  48300  linccl  48331  lincvalpr  48335  lincresunit3lem1  48396  lincresunit3  48398  fdivmpt  48461  nnolog2flm1  48511  dignnld  48524  digexp  48528  dignn0flhalflem1  48536  itcovalsucov  48589  reorelicc  48631  eenglngeehlnmlem1  48658  line2  48673  line2xlem  48674  itsclc0lem1  48677  itsclc0xyqsolr  48690  i0oii  48817  io1ii  48818  indthinc  49109  indthincALT  49110  setrec2fun  49211  reccot  49277  rectan  49278