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  2628  vtoclegftOLD  3546  eqeu  3668  onunel  6418  iotan0  6476  funopg  6520  dff1o2  6773  fvelimad  6894  unima  6902  fnimapr  6910  fvmptt  6954  fnreseql  6986  xpprsng  7078  f1elima  7204  f1ounsn  7213  f13dfv  7215  f1ocnvfvb  7220  f1cdmsn  7223  f1ofvswap  7247  oprssov  7522  resf1extb  7874  resf1ext2b  7875  funelss  7989  poxp  8068  poxp2  8083  poxp3  8090  smoiso  8292  oaord  8472  oaword  8474  omcan  8494  omwordri  8497  odi  8504  omeulem1  8507  oeord  8513  oecan  8514  oewordri  8517  oeordsuc  8519  nnaord  8544  nnaordr  8545  nndi  8548  nnaword  8552  nnmwordri  8561  naddel2  8613  naddss1  8614  naddss2  8615  erov  8748  ecopovtrn  8754  mapsnd  8820  f1dom3g  8900  xpdom3  8999  mapxpen  9067  dif1en  9084  dif1enOLD  9086  findcard  9087  f1domfi2  9106  entrfir  9115  domtrfil  9116  domtrfir  9118  sbthfilem  9122  sdomdomtrfi  9125  php3  9133  findcard3  9187  indexfi  9269  suppr  9381  infpr  9414  r111  9690  tcrank  9799  acndom  9964  infdif2  10122  infxpdom  10123  cfeq0  10169  cfsuc  10170  cfflb  10172  cflim2  10176  cfsmolem  10183  axcc3  10351  domtriomlem  10355  axdc3lem2  10364  axdc3lem4  10366  axdc4lem  10368  axcclem  10370  pwcfsdom  10496  tsktrss  10674  tsksuc  10675  tskuni  10696  adderpqlem  10867  mulerpqlem  10868  mulcanenq  10873  distrnq  10874  ltsonq  10882  ltanq  10884  ltmnq  10885  distrlem1pr  10938  distrlem5pr  10940  ltsopr  10945  ltsosr  11007  ltasr  11013  adddir  11125  axlttrn  11206  letr  11228  nnncan1  11418  npncan3  11420  pnpcan2  11422  subdi  11571  subdir  11572  mulcan1g  11791  mulcan2g  11792  divmul  11800  div23  11816  div13  11818  muldivdir  11835  divsubdir  11836  subdivcomb1  11837  divcan7  11851  ltmul2  11993  lemul1  11994  lemul2  11995  lemul2a  11997  lediv1  12008  ltmuldiv2  12017  lemuldiv  12023  lemuldiv2  12024  ltdiv2  12029  lediv2  12033  infrelb  12128  nndivtr  12193  bndndx  12401  nn0n0n1ge2  12470  fnn0ind  12593  addlelt  13027  xrletr  13078  qsqueeze  13121  xleadd2a  13174  xleadd1  13175  xltadd2  13177  xltmul2  13213  supxrbnd  13248  iooneg  13392  iccneg  13393  icoshft  13394  icoshftf1o  13395  zltaddlt1le  13426  fzen  13462  uzsubsubfz  13467  ssfzunsnext  13490  fzrevral2  13534  fzshftral  13536  fz0fzdiffz0  13558  elfzmlbp  13560  elfzo  13582  nelfzo  13585  fzoaddel2  13641  fzosubel2  13646  ssfzo12bi  13682  fzonfzoufzol  13691  subfzo0  13710  flltdivnn0lt  13755  modmulnn  13811  modcyc  13828  modaddabs  13833  modaddmod  13834  modmuladd  13838  modadd2mod  13846  modsubmod  13854  modsubmodmod  13855  modaddmodup  13859  modmulmod  13861  modsubdir  13865  modfzo0difsn  13868  modsumfzodifsn  13869  uzindi  13907  axdc4uzlem  13908  expneg2  13995  expdiv  14038  expubnd  14103  mulbinom2  14148  bernneq2  14155  expnngt1  14166  hashinfxadd  14310  hashunsngx  14318  hashunsnggt  14319  hashfundm  14367  hashf1dmcdm  14369  hashdifsnp1  14431  ccatval3  14504  ccatfv0  14508  ccatval1lsw  14509  ccats1val2  14552  ccatw2s1p1  14561  swrdnd  14579  pfxsuffeqwrdeq  14622  pfxsuff1eqwrdeq  14623  swrdswrd  14629  pfxpfx  14632  wrd2ind  14647  swrdccatin1  14649  pfxccatin12lem1  14652  swrdccatin2  14653  pfxccatin12lem3  14656  swrdccat  14659  pfxccatpfx1  14660  pfxccatpfx2  14661  swrdccat3blem  14663  repswswrd  14708  repswpfx  14709  repswccat  14710  cshwidxmod  14727  2cshw  14737  3cshw  14742  scshwfzeqfzo  14751  cshwcsh2id  14753  cshimadifsn  14754  cshimadifsn0  14755  ccatco  14760  cshco  14761  swrdco  14762  pfxco  14763  lswco  14764  swrds2  14865  2swrd2eqwrdeq  14878  shftuz  14994  abs3dif  15257  fsumdifsnconst  15716  modfsummods  15718  sin02gt0  16119  dvdsval2  16184  dvdscmul  16211  dvdsmulc  16212  dvdscmulr  16213  dvdsmulcr  16214  divalglem8  16329  ndvdssub  16338  dvdsexpim  16484  rpmulgcd  16486  expgcd  16492  zexpgcd  16494  coprmprod  16590  cncongr1  16596  cncongr2  16597  isprm3  16612  modprm0  16735  coprimeprodsq  16738  pythagtriplem12  16756  pythagtriplem14  16758  pcprendvds  16770  pcmul  16781  pcdiv  16782  pcqcl  16786  pcqdiv  16787  pcdvdsb  16799  vdwnnlem1  16925  hashbcss  16934  cshwshashlem1  17025  fvsetsid  17097  setsstruct2  17103  setsstruct  17105  mrcss  17540  mrcsscl  17544  mrcun  17546  cofulid  17815  catcisolem  18035  funcsetcestrclem9  18087  latleeqj1  18375  lubun  18439  clatleglb  18442  pslem  18496  dirtr  18526  mgmb1mgm1  18547  pwspjmhm  18722  grpinvid1  18888  grpinvid2  18889  grpasscan1  18898  grpasscan2  18899  grpinvadd  18915  grpsubf  18916  grpsubrcan  18918  grpinvsub  18919  grpsubeq0  18923  grpsubadd0sub  18924  grppncan  18928  grpnpcan  18929  mulgnn0p1  18982  mulgaddcomlem  18994  mulginvcom  18996  mulginvinv  18997  subgsubcl  19034  subgsub  19035  eqglact  19076  qussub  19088  ghmsub  19121  psgnunilem4  19394  oddvds2  19463  odsubdvds  19468  gexnnod  19485  slwn0  19512  dvrcl  20307  unitdvcl  20308  dvrcan1  20312  dvrcan3  20313  dvreq1  20314  rngisom1  20369  rngisomring  20370  subrgdv  20492  abvsubtri  20730  idsrngd  20759  lmodvsubval2  20838  lsmcl  21005  lsmsp2  21009  lspsntrim  21020  rngqiprngimfolem  21215  lidldvgen  21259  cncrng  21313  chrcong  21452  dvdschrmulg  21453  zndvds  21474  zntoslem  21481  ocvsscon  21600  obselocv  21653  frlmphl  21706  ascldimul  21813  mpfsubrg  22026  ply1tmcl  22174  eqcoe1ply1eq  22202  gsummoncoe1  22211  lply1binomsc  22214  mamudm  22298  mamufacex  22299  scmatf1  22434  scmatf1o  22435  scmatrngiso  22439  submabas  22481  mdetdiaglem  22501  mdetralt2  22512  mdetero  22513  mdetunilem2  22516  mdetunilem6  22520  m2detleiblem7  22530  maducoeval2  22543  gsummatr01lem3  22560  gsummatr01  22562  smadiadetglem2  22575  cramerlem1  22590  mply1topmatcl  22708  mp2pm2mplem4  22712  ntrin  22964  elnei  23014  neindisj2  23026  ordtopn3  23099  leordtval2  23115  lecldbas  23122  cnrest2  23189  cmpsublem  23302  ptrescn  23542  xkococn  23563  kqfeq  23627  snfbas  23769  neifil  23783  fclsrest  23927  utopsnnei  24153  neipcfilu  24199  psmetsym  24214  psmetge0  24216  xmetge0  24248  xmetsym  24251  metustto  24457  metustbl  24470  restmetu  24474  nm2dif  24529  nmtri  24530  cnmet  24675  cnmpopc  24838  iihalf1  24841  iihalf2  24844  iocopnst  24853  clmnegsubdi2  25021  clmsub4  25022  clmvsubval2  25026  ncvspi  25072  cphsqrtcl3  25103  cph2ass  25129  cphipval2  25157  cphipval  25159  caublcls  25225  bcthlem3  25242  bcthlem4  25243  srabn  25276  cssbn  25291  cmslsschl  25293  rrxmet  25324  rrxdsfi  25327  iblconst  25735  dvdsq1p  26084  coeid3  26161  aannenlem2  26253  pserdvlem2  26354  tanord1  26462  cxpef  26590  recxpcl  26600  logbchbase  26697  relogbcl  26699  relogbzcl  26700  logbleb  26709  logblt  26710  relogbcxpb  26713  lawcos  26742  pythag  26743  isosctrlem1  26744  isosctrlem2  26745  lgsmodeq  27269  lgsmulsqcoprm  27270  gausslemma2dlem1a  27292  2lgsoddprmlem2  27336  sltres  27590  sletr  27686  cofcutr  27855  lrrecpo  27871  sltadd2im  27916  sleadd2im  27918  sleadd1  27919  sleadd2  27920  sltadd1  27922  addscan2  27923  addscan1  27924  sltsub1  28003  divsmulw  28119  zsoring  28319  ax5seglem1  28891  axcontlem2  28928  axcontlem8  28934  upgrpredgv  29102  numedglnl  29107  issubgr2  29235  uhgrissubgr  29238  egrsubgr  29240  nbusgrfi  29337  nb3grprlem2  29344  cplgr3v  29398  cusgrsizeindslem  29415  finsumvtxdg2size  29514  rusgrpropadjvtx  29549  upgrwlkvtxedg  29608  usgr2trlncl  29723  uspgrn2crct  29771  crctcshwlkn0lem4  29776  crctcshwlkn0lem5  29777  wwlksnextproplem3  29874  umgr2adedgwlklem  29907  rusgr0edg  29936  clwwlk1loop  29950  clwwlkccatlem  29951  clwlkclwwlklem2a4  29959  clwlkclwwlklem2a  29960  clwwisshclwwslemlem  29975  erclwwlktr  29984  clwwlkel  30008  erclwwlkntr  30033  clwwlknonex2lem2  30070  uhgr3cyclex  30144  umgr3cyclex  30145  eucrctshift  30205  frgr3v  30237  3cyclfrgrrn  30248  frgrwopreglem5a  30273  frgr2wsp1  30292  extwwlkfab  30314  clwwlknonclwlknonf1o  30324  numclwwlk3lem1  30344  numclwwlk5  30350  numclwwlk6  30352  isgrpo  30459  grpoinvid1  30490  grpoinvid2  30491  grpoinvop  30495  grpodivinv  30498  grpoinvdiv  30499  grpodivf  30500  grponpcan  30505  ablonncan  30518  nvmval  30604  nvmval2  30605  nvmfval  30606  nvmul0or  30612  nvpncan2  30615  nvaddsub4  30619  nvmeq0  30620  nvdif  30628  nvpi  30629  nvmtri  30633  nvabs  30634  imsmetlem  30652  ipval2lem3  30667  ipval2  30669  4ipval2  30670  ipval3  30671  nmooge0  30729  blometi  30765  hvaddsub12  31000  hvsubdistr1  31011  hvsubdistr2  31012  hvaddcan2  31033  hvmulcan  31034  hvmulcan2  31035  hvsubcan  31036  hvsubcan2  31037  his7  31052  his2sub  31054  his2sub2  31055  norm3dif2  31113  shsubcl  31182  hhssnv  31226  shlej2  31323  fh2  31581  cm2j  31582  pjoi0  31679  hodcl  31709  hosubdi  31770  unopf1o  31878  unopadj  31881  adj2  31896  braadd  31907  bramul  31908  lnopaddmuli  31935  lnopsubmuli  31937  homco2  31939  lnfnaddmuli  32007  adjlnop  32048  leopmul  32096  leoptr  32099  pjimai  32138  atcv1  32342  atexch  32343  atcvatlem  32347  fcoinvbr  32567  preiman0  32666  divnumden2  32773  sgn3da  32792  xdivmul  32878  cshf1o  32917  resvsca  33283  idlsrgcmnd  33465  hasheuni  34054  difelsiga  34102  cndprobin  34404  bayesth  34409  signstfvp  34541  breprexplemc  34602  fineqvac  35074  swrdrevpfx  35092  swrdwlk  35102  lediv2aALT  35652  fununiq  35744  dfrdg2  35771  clsun  36304  neiin  36308  rdgeqoa  37346  curfv  37582  matunitlindflem1  37598  poimirlem32  37634  ftc1anclem4  37678  areacirc  37695  filbcmb  37722  ismtybnd  37789  grpoeqdivid  37863  ghomco  37873  rngonegrmul  37926  zerdivemp1x  37929  rngohomco  37956  rngoisoco  37964  riscer  37970  intidl  38011  isfldidl  38050  eceldmqsxrncnvepres  38386  eceldmqsxrncnvepres2  38387  brredunds  38605  lshpnelb  38965  opnlen0  39169  opcon3b  39177  opcon2b  39178  oplecon3b  39181  opltcon3b  39185  opltcon2b  39187  oldmm1  39198  oldmm4  39201  oldmj1  39202  oldmj4  39205  cvrval2  39255  cvrcon3b  39258  leatb  39273  atcmp  39292  atcvreq0  39295  atlatle  39301  athgt  39438  3dim2  39450  islln2a  39499  lplnnleat  39524  lvolnleat  39565  4atlem10  39588  4atlem11  39591  4atlem12  39594  dalem21  39676  dalem22  39677  dalem23  39678  dalem29  39683  dalem30  39684  dalem31N  39685  dalem32  39686  dalem33  39687  dalem34  39688  dalem35  39689  dalem36  39690  dalem37  39691  dalem40  39694  dalem46  39700  dalem47  39701  dalem51  39705  dalem52  39706  dalem58  39712  dalem59  39713  pmaple  39743  paddclN  39824  pmapjoin  39834  pmapjat1  39835  elpcliN  39875  pclssN  39876  pclun2N  39881  2polcon4bN  39900  paddunN  39909  poldmj1N  39910  pmapj2N  39911  pmapocjN  39912  psubclinN  39930  paddatclN  39931  poml4N  39935  lautco  40079  ldilco  40098  ltrneq2  40130  trljat1  40148  cdlemc1  40173  cdleme10  40236  ltrnco  40701  trlcocnv  40702  trljco  40722  trljco2  40723  cdlemi1  40800  tendocnv  41003  diaord  41029  dibord  41141  dihord3  41239  dihord4  41240  dihmeetlem2N  41281  dihmeetlem4preN  41288  dochdmj1  41372  hdmap10lem  41821  lcmineqlem1  42005  sticksstones2  42123  readdsub  42360  reltsub1  42362  renpncan3  42367  reppncan  42369  resubdi  42372  readdcan2  42389  mzprename  42725  dvdsrabdioph  42786  pell14qrdivcl  42841  monotoddzz  42919  jm2.19lem2  42966  jm2.19  42969  relexpaddss  43694  k0004lem3  44125  dvconstbi  44310  chordthmALT  44909  isosctrlem1ALT  44910  ssinc  45068  ssdec  45069  wessf1ornlem  45166  disjf1o  45172  ssnnf1octb  45175  projf1o  45178  mapssbi  45194  iunmapsn  45198  upbdrech  45290  iuneqfzuzlem  45317  suplesup  45322  rexabslelem  45401  climxrrelem  45734  limsupresxr  45751  liminfresxr  45752  liminfvalxr  45768  xlimliminflimsup  45847  cncfshift  45859  cncfperiod  45864  cncfuni  45871  icccncfext  45872  dvmptfprodlem  45929  dvnprodlem1  45931  itgspltprt  45964  ismbl3  45971  stoweidlem3  45988  stoweidlem10  45995  stoweidlem19  46004  stoweidlem31  46016  stoweidlem34  46019  stoweidlem44  46029  fourierdlem41  46133  fourierdlem42  46134  fourierdlem51  46142  fourierdlem68  46159  fourierdlem89  46180  fourierdlem91  46182  fourierdlem92  46183  fourierdlem94  46185  etransclem24  46243  etransclem34  46253  qndenserrnbllem  46279  salincl  46309  saldifcl2  46313  subsalsal  46344  sge0pr  46379  sge0pnffigt  46381  sge0reuz  46432  nnfoctbdjlem  46440  nnfoctbdj  46441  meadjiunlem  46450  caratheodorylem2  46512  hoidmv1le  46579  hoidmvlelem3  46582  hspmbllem2  46612  opnvonmbllem2  46618  sssmf  46723  smfaddlem1  46748  sigaraf  46838  sigarmf  46839  nltle2tri  47301  subsubelfzo0  47314  submodaddmod  47329  zplusmodne  47331  addmodne  47332  minusmod5ne  47337  submodneaddmod  47339  modmkpkne  47349  modmknepk  47350  iccpartiltu  47410  icceuelpart  47424  poprelb  47512  reuopreuprim  47514  proththd  47602  mogoldbblem  47708  fppr2odd  47719  fpprel2  47729  bgoldbtbndlem2  47794  clnbusgrfi  47831  grimuhgr  47875  uhgrimisgrgric  47919  clnbgrgrim  47922  grtrif1o  47930  grlimgrtri  47991  gpgusgralem  48044  gpgedgvtx0  48049  gpgedg2ov  48054  gpgedg2iv  48055  gpg5nbgrvtx03starlem2  48057  nn0sumltlt  48338  invginvrid  48355  ply1sclrmsm  48372  linccl  48403  lincvalpr  48407  lincresunit3lem1  48468  lincresunit3  48470  fdivmpt  48529  nnolog2flm1  48579  dignnld  48592  digexp  48596  dignn0flhalflem1  48604  itcovalsucov  48657  reorelicc  48699  eenglngeehlnmlem1  48726  line2  48741  line2xlem  48742  itsclc0lem1  48745  itsclc0xyqsolr  48758  i0oii  48908  io1ii  48909  indthinc  49451  indthincALT  49452  setrec2fun  49681  reccot  49747  rectan  49748