Theorem 3adant2 1130

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  3ad2ant1  1132  3simpb  1148  3imp3i2an  1344  eupickb  2638  vtoclegft  3523  eqeu  3642  iotan0  6427  funopg  6475  fncoOLD  6559  dff1o2  6730  fvelimad  6845  unima  6852  fnimapr  6861  fvmptt  6904  fnreseql  6934  xpprsng  7021  f1elima  7145  f13dfv  7155  f1ocnvfvb  7160  f1cdmsn  7163  f1ofvswap  7187  oprssov  7450  funelss  7897  poxp  7978  wfrlem4OLD  8152  smoiso  8202  oaord  8387  oaword  8389  omcan  8409  omwordri  8412  odi  8419  omeulem1  8422  oeord  8428  oecan  8429  oewordri  8432  oeordsuc  8434  nnaord  8459  nnaordr  8460  nndi  8463  nnaword  8467  nnmwordri  8476  erov  8612  ecopovtrn  8618  mapsnd  8683  f1dom3g  8764  xpdom3  8866  mapxpen  8939  dif1en  8954  findcard  8955  f1domfi2  8977  entrfir  8986  domtrfil  8987  domtrfir  8989  sbthfilem  8993  sdomdomtrfi  8996  php3  9004  indexfi  9136  suppr  9239  infpr  9271  r111  9542  tcrank  9651  acndom  9816  infdif2  9975  infxpdom  9976  cfeq0  10021  cfsuc  10022  cfflb  10024  cflim2  10028  cfsmolem  10035  axcc3  10203  domtriomlem  10207  axdc3lem2  10216  axdc3lem4  10218  axdc4lem  10220  axcclem  10222  pwcfsdom  10348  tsktrss  10526  tsksuc  10527  tskuni  10548  adderpqlem  10719  mulerpqlem  10720  mulcanenq  10725  distrnq  10726  ltsonq  10734  ltanq  10736  ltmnq  10737  distrlem1pr  10790  distrlem5pr  10792  ltsopr  10797  ltsosr  10859  ltasr  10865  adddir  10975  axlttrn  11056  letr  11078  nnncan1  11266  npncan3  11268  pnpcan2  11270  subdi  11417  subdir  11418  mulcan1g  11637  mulcan2g  11638  divmul  11645  div23  11661  div13  11663  muldivdir  11677  divsubdir  11678  subdivcomb1  11679  divcan7  11693  ltmul2  11835  lemul1  11836  lemul2  11837  lemul2a  11839  lediv1  11849  ltmuldiv2  11858  lemuldiv  11864  lemuldiv2  11865  ltdiv2  11870  lediv2  11874  infrelb  11969  nndivtr  12029  bndndx  12241  nn0n0n1ge2  12309  fnn0ind  12428  addlelt  12853  xrletr  12901  qsqueeze  12944  xleadd2a  12997  xleadd1  12998  xltadd2  13000  xltmul2  13036  supxrbnd  13071  iooneg  13212  iccneg  13213  icoshft  13214  icoshftf1o  13215  zltaddlt1le  13246  fzen  13282  uzsubsubfz  13287  ssfzunsnext  13310  fzrevral2  13351  fzshftral  13353  fz0fzdiffz0  13374  elfzmlbp  13376  elfzo  13398  nelfzo  13401  fzoaddel2  13452  fzosubel2  13456  ssfzo12bi  13491  fzonfzoufzol  13499  subfzo0  13518  flltdivnn0lt  13562  modmulnn  13618  modcyc  13635  modaddabs  13638  modaddmod  13639  modmuladd  13642  modadd2mod  13650  modsubmod  13658  modsubmodmod  13659  modaddmodup  13663  modmulmod  13665  modsubdir  13669  modfzo0difsn  13672  modsumfzodifsn  13673  uzindi  13711  axdc4uzlem  13712  expneg2  13800  expdiv  13843  expubnd  13904  mulbinom2  13947  bernneq2  13954  expnngt1  13965  hashinfxadd  14109  hashunsngx  14117  hashunsnggt  14118  hashdifsnp1  14219  ccatval3  14293  ccatfv0  14297  ccatval1lsw  14298  ccats1val2  14343  ccatw2s1p1  14355  swrdnd  14376  pfxsuffeqwrdeq  14420  pfxsuff1eqwrdeq  14421  swrdswrd  14427  pfxpfx  14430  wrd2ind  14445  swrdccatin1  14447  pfxccatin12lem1  14450  swrdccatin2  14451  pfxccatin12lem3  14454  swrdccat  14457  pfxccatpfx1  14458  pfxccatpfx2  14459  swrdccat3blem  14461  repswswrd  14506  repswpfx  14507  repswccat  14508  cshwidxmod  14525  2cshw  14535  3cshw  14540  scshwfzeqfzo  14548  cshwcsh2id  14550  cshimadifsn  14551  cshimadifsn0  14552  ccatco  14557  cshco  14558  swrdco  14559  pfxco  14560  lswco  14561  swrds2  14662  2swrd2eqwrdeq  14675  shftuz  14789  abs3dif  15052  fsumdifsnconst  15512  modfsummods  15514  sin02gt0  15910  dvdsval2  15975  dvdscmul  16001  dvdsmulc  16002  dvdscmulr  16003  dvdsmulcr  16004  divalglem8  16118  ndvdssub  16127  rpmulgcd  16275  coprmprod  16375  cncongr1  16381  cncongr2  16382  isprm3  16397  modprm0  16515  coprimeprodsq  16518  pythagtriplem12  16536  pythagtriplem14  16538  pcprendvds  16550  pcmul  16561  pcdiv  16562  pcqcl  16566  pcqdiv  16567  pcdvdsb  16579  vdwnnlem1  16705  hashbcss  16714  cshwshashlem1  16806  fvsetsid  16878  setsstruct2  16884  setsstruct  16886  mrcss  17334  mrcsscl  17338  mrcun  17340  cofulid  17614  catcisolem  17834  funcsetcestrclem9  17889  latleeqj1  18178  lubun  18242  clatleglb  18245  pslem  18299  dirtr  18329  mgmb1mgm1  18348  pwspjmhm  18477  grpinvid1  18639  grpinvid2  18640  grpasscan1  18647  grpasscan2  18648  grpinvadd  18662  grpsubf  18663  grpsubrcan  18665  grpinvsub  18666  grpsubeq0  18670  grpsubadd0sub  18671  grppncan  18675  grpnpcan  18676  mulgnn0p1  18724  mulgaddcomlem  18735  mulginvcom  18737  mulginvinv  18738  subgsubcl  18775  subgsub  18776  eqglact  18816  qussub  18825  ghmsub  18851  psgnunilem4  19114  oddvds2  19182  odsubdvds  19185  gexnnod  19202  slwn0  19229  dvrcl  19937  unitdvcl  19938  dvrcan1  19942  dvrcan3  19943  dvreq1  19944  subrgdv  20050  abvsubtri  20104  idsrngd  20131  lmodvsubval2  20187  lsmcl  20354  lsmsp2  20358  lspsntrim  20369  lidldvgen  20535  chrcong  20742  zndvds  20766  zntoslem  20773  ocvsscon  20889  obselocv  20944  frlmphl  20997  ascldimul  21101  mpfsubrg  21322  ply1tmcl  21452  eqcoe1ply1eq  21477  gsummoncoe1  21484  lply1binomsc  21487  mamudm  21546  mamufacex  21547  scmatf1  21689  scmatf1o  21690  scmatrngiso  21694  submabas  21736  mdetdiaglem  21756  mdetralt2  21767  mdetero  21768  mdetunilem2  21771  mdetunilem6  21775  m2detleiblem7  21785  maducoeval2  21798  gsummatr01lem3  21815  gsummatr01  21817  smadiadetglem2  21830  cramerlem1  21845  mply1topmatcl  21963  mp2pm2mplem4  21967  ntrin  22221  elnei  22271  neindisj2  22283  ordtopn3  22356  leordtval2  22372  lecldbas  22379  cnrest2  22446  cmpsublem  22559  ptrescn  22799  xkococn  22820  kqfeq  22884  snfbas  23026  neifil  23040  fclsrest  23184  utopsnnei  23410  neipcfilu  23457  psmetsym  23472  psmetge0  23474  xmetge0  23506  xmetsym  23509  metustto  23718  metustbl  23731  restmetu  23735  nm2dif  23790  nmtri  23791  cnmet  23944  cnmpopc  24100  iihalf1  24103  iihalf2  24105  iocopnst  24112  clmnegsubdi2  24277  clmsub4  24278  clmvsubval2  24282  ncvspi  24329  cphsqrtcl3  24360  cph2ass  24386  cphipval2  24414  cphipval  24416  caublcls  24482  bcthlem3  24499  bcthlem4  24500  srabn  24533  cssbn  24548  cmslsschl  24550  rrxmet  24581  rrxdsfi  24584  iblconst  24991  tdeglem3OLD  25232  dvdsq1p  25334  coeid3  25410  aannenlem2  25498  pserdvlem2  25596  tanord1  25702  cxpef  25829  recxpcl  25839  logbchbase  25930  relogbcl  25932  relogbzcl  25933  logbleb  25942  logblt  25943  relogbcxpb  25946  lawcos  25975  pythag  25976  isosctrlem1  25977  isosctrlem2  25978  lgsmodeq  26499  lgsmulsqcoprm  26500  gausslemma2dlem1a  26522  2lgsoddprmlem2  26566  ax5seglem1  27305  axcontlem2  27342  axcontlem8  27348  upgrpredgv  27518  numedglnl  27523  issubgr2  27648  uhgrissubgr  27651  egrsubgr  27653  nbusgrfi  27750  nb3grprlem2  27757  cplgr3v  27811  cusgrsizeindslem  27827  finsumvtxdg2size  27926  rusgrpropadjvtx  27961  upgrwlkvtxedg  28021  usgr2trlncl  28137  uspgrn2crct  28182  crctcshwlkn0lem4  28187  crctcshwlkn0lem5  28188  wwlksnextproplem3  28285  umgr2adedgwlklem  28318  rusgr0edg  28347  clwwlk1loop  28361  clwwlkccatlem  28362  clwlkclwwlklem2a4  28370  clwlkclwwlklem2a  28371  clwwisshclwwslemlem  28386  erclwwlktr  28395  clwwlkel  28419  erclwwlkntr  28444  clwwlknonex2lem2  28481  uhgr3cyclex  28555  umgr3cyclex  28556  eucrctshift  28616  frgr3v  28648  3cyclfrgrrn  28659  frgrwopreglem5a  28684  frgr2wsp1  28703  extwwlkfab  28725  clwwlknonclwlknonf1o  28735  numclwwlk3lem1  28755  numclwwlk5  28761  numclwwlk6  28763  isgrpo  28868  grpoinvid1  28899  grpoinvid2  28900  grpoinvop  28904  grpodivinv  28907  grpoinvdiv  28908  grpodivf  28909  grponpcan  28914  ablonncan  28927  nvmval  29013  nvmval2  29014  nvmfval  29015  nvmul0or  29021  nvpncan2  29024  nvaddsub4  29028  nvmeq0  29029  nvdif  29037  nvpi  29038  nvmtri  29042  nvabs  29043  imsmetlem  29061  ipval2lem3  29076  ipval2  29078  4ipval2  29079  ipval3  29080  nmooge0  29138  blometi  29174  hvaddsub12  29409  hvsubdistr1  29420  hvsubdistr2  29421  hvaddcan2  29442  hvmulcan  29443  hvmulcan2  29444  hvsubcan  29445  hvsubcan2  29446  his7  29461  his2sub  29463  his2sub2  29464  norm3dif2  29522  shsubcl  29591  hhssnv  29635  shlej2  29732  fh2  29990  cm2j  29991  pjoi0  30088  hodcl  30118  hosubdi  30179  unopf1o  30287  unopadj  30290  adj2  30305  braadd  30316  bramul  30317  lnopaddmuli  30344  lnopsubmuli  30346  homco2  30348  lnfnaddmuli  30416  adjlnop  30457  leopmul  30505  leoptr  30508  pjimai  30547  atcv1  30751  atexch  30752  atcvatlem  30756  fcoinvbr  30956  preiman0  31051  divnumden2  31141  xdivmul  31208  cshf1o  31243  dvdschrmulg  31492  resvsca  31538  idlsrgcmnd  31669  hasheuni  32062  difelsiga  32110  cndprobin  32410  bayesth  32415  sgn3da  32517  signstfvp  32559  breprexplemc  32621  fineqvac  33075  hashfundm  33083  hashf1dmcdm  33085  swrdrevpfx  33087  swrdwlk  33097  lediv2aALT  33644  onunel  33698  fununiq  33752  dfrdg2  33780  poxp2  33799  poxp3  33805  naddel2  33849  naddss1  33850  naddss2  33851  sltres  33874  sletr  33970  cofcutr  34101  lrrecpo  34107  clsun  34526  neiin  34530  rdgeqoa  35550  curfv  35766  matunitlindflem1  35782  poimirlem32  35818  ftc1anclem4  35862  areacirc  35879  filbcmb  35907  ismtybnd  35974  grpoeqdivid  36048  ghomco  36058  rngonegrmul  36111  zerdivemp1x  36114  rngohomco  36141  rngoisoco  36149  riscer  36155  intidl  36196  isfldidl  36235  brredunds  36746  lshpnelb  37005  opnlen0  37209  opcon3b  37217  opcon2b  37218  oplecon3b  37221  opltcon3b  37225  opltcon2b  37227  oldmm1  37238  oldmm4  37241  oldmj1  37242  oldmj4  37245  cvrval2  37295  cvrcon3b  37298  leatb  37313  atcmp  37332  atcvreq0  37335  atlatle  37341  athgt  37477  3dim2  37489  islln2a  37538  lplnnleat  37563  lvolnleat  37604  4atlem10  37627  4atlem11  37630  4atlem12  37633  dalem21  37715  dalem22  37716  dalem23  37717  dalem29  37722  dalem30  37723  dalem31N  37724  dalem32  37725  dalem33  37726  dalem34  37727  dalem35  37728  dalem36  37729  dalem37  37730  dalem40  37733  dalem46  37739  dalem47  37740  dalem51  37744  dalem52  37745  dalem58  37751  dalem59  37752  pmaple  37782  paddclN  37863  pmapjoin  37873  pmapjat1  37874  elpcliN  37914  pclssN  37915  pclun2N  37920  2polcon4bN  37939  paddunN  37948  poldmj1N  37949  pmapj2N  37950  pmapocjN  37951  psubclinN  37969  paddatclN  37970  poml4N  37974  lautco  38118  ldilco  38137  ltrneq2  38169  trljat1  38187  cdlemc1  38212  cdleme10  38275  ltrnco  38740  trlcocnv  38741  trljco  38761  trljco2  38762  cdlemi1  38839  tendocnv  39042  diaord  39068  dibord  39180  dihord3  39278  dihord4  39279  dihmeetlem2N  39320  dihmeetlem4preN  39327  dochdmj1  39411  hdmap10lem  39860  lcmineqlem1  40044  sticksstones2  40110  metakunt29  40160  metakunt30  40161  factwoffsmonot  40170  dvdsexpim  40335  expgcd  40341  zexpgcd  40343  readdsub  40374  reltsub1  40376  renpncan3  40381  reppncan  40383  resubdi  40386  readdcan2  40402  mzprename  40578  dvdsrabdioph  40639  pell14qrdivcl  40694  monotoddzz  40772  jm2.19lem2  40819  jm2.19  40822  relexpaddss  41333  k0004lem3  41766  dvconstbi  41959  chordthmALT  42560  isosctrlem1ALT  42561  ssinc  42644  ssdec  42645  wessf1ornlem  42729  disjf1o  42736  ssnnf1octb  42740  projf1o  42743  mapssbi  42760  iunmapsn  42764  upbdrech  42851  iuneqfzuzlem  42880  suplesup  42885  rexabslelem  42965  climxrrelem  43297  limsupresxr  43314  liminfresxr  43315  liminfvalxr  43331  xlimliminflimsup  43410  cncfshift  43422  cncfperiod  43427  cncfuni  43434  icccncfext  43435  dvmptfprodlem  43492  dvnprodlem1  43494  itgspltprt  43527  ismbl3  43534  stoweidlem3  43551  stoweidlem10  43558  stoweidlem19  43567  stoweidlem31  43579  stoweidlem34  43582  stoweidlem44  43592  fourierdlem41  43696  fourierdlem42  43697  fourierdlem51  43705  fourierdlem68  43722  fourierdlem89  43743  fourierdlem91  43745  fourierdlem92  43746  fourierdlem94  43748  etransclem24  43806  etransclem34  43816  qndenserrnbllem  43842  salincl  43871  saldifcl2  43874  subsalsal  43905  sge0pr  43939  sge0pnffigt  43941  sge0reuz  43992  nnfoctbdjlem  44000  nnfoctbdj  44001  meadjiunlem  44010  caratheodorylem2  44072  hoidmv1le  44139  hoidmvlelem3  44142  hspmbllem2  44172  opnvonmbllem2  44178  sssmf  44283  smfaddlem1  44308  sigaraf  44380  sigarmf  44381  nltle2tri  44816  subsubelfzo0  44829  iccpartiltu  44885  icceuelpart  44899  poprelb  44987  reuopreuprim  44989  proththd  45077  mogoldbblem  45183  fppr2odd  45194  fpprel2  45204  bgoldbtbndlem2  45269  isomgrtr  45302  nn0sumltlt  45697  invginvrid  45714  ply1sclrmsm  45735  linccl  45766  lincvalpr  45770  lincresunit3lem1  45831  lincresunit3  45833  fdivmpt  45897  nnolog2flm1  45947  dignnld  45960  digexp  45964  dignn0flhalflem1  45972  itcovalsucov  46025  reorelicc  46067  eenglngeehlnmlem1  46094  line2  46109  line2xlem  46110  itsclc0lem1  46113  itsclc0xyqsolr  46126  i0oii  46224  io1ii  46225  indthinc  46344  indthincALT  46345  setrec2fun  46409  reccot  46471  rectan  46472