Theorem 3adant2 1149

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3ad2ant1  1151  3simpb  1167  3imp3i2an  1364  eupickb  2660  eqeu  3664  onunel  6465  iotan0  6523  funopg  6567  dff1o2  6823  fvelimad  6945  unima  6953  fnimapr  6961  fvmptt  7007  fnreseql  7040  xpprsng  7135  xpsnprg  7136  f1elima  7260  f1ounsn  7273  f13dfv  7275  f1ocnvfvb  7280  f1cdmsn  7283  f1ofvswap  7307  oprssov  7583  resf1extb  7931  resf1ext2b  7932  funelss  8044  poxp  8126  poxp2  8141  poxp3  8148  smoiso  8351  oaord  8534  oaword  8536  omcan  8556  omwordri  8559  odi  8566  omeulem1  8569  oeord  8576  oecan  8577  oewordri  8580  oeordsuc  8582  nnaord  8607  nnaordr  8608  nndi  8611  nnaword  8615  nnmwordri  8624  naddel2  8677  naddss1  8678  naddss2  8679  erov  8814  ecopovtrn  8820  curfv  8871  mapsnd  8893  f1dom3g  8973  xpdom3  9073  mapxpen  9141  dif1en  9156  findcard  9158  f1domfi2  9176  entrfir  9185  domtrfil  9186  domtrfir  9188  sbthfilem  9192  sdomdomtrfi  9195  php3  9203  findcard3  9253  indexfi  9327  suppr  9442  infpr  9475  r111  9757  tcrank  9866  acndom  10054  infdif2  10211  infxpdom  10212  cfeq0  10258  cfsuc  10259  cfflb  10261  cflim2  10265  cfsmolem  10272  axcc3  10440  domtriomlem  10444  axdc3lem2  10453  axdc3lem4  10455  axdc4lem  10457  axcclem  10459  pwcfsdom  10592  tsktrss  10770  tsksuc  10771  tskuni  10792  adderpqlem  10963  mulerpqlem  10964  mulcanenq  10969  distrnq  10970  ltsonq  10978  ltanq  10980  ltmnq  10981  distrlem1pr  11034  distrlem5pr  11036  ltsopr  11041  ltsosr  11103  ltasr  11109  adddir  11221  axlttrn  11306  letr  11328  nnncan1  11518  npncan3  11520  pnpcan2  11522  subdi  11671  subdir  11672  mulcan1g  11891  mulcan2g  11892  divmul  11899  div23  11915  div13  11917  muldivdir  11931  divsubdir  11932  subdivcomb1  11934  divcan7  11948  ltmul2  12090  lemul1  12091  lemul2  12092  lemul2a  12094  lediv1  12104  ltmuldiv2  12113  lemuldiv  12119  lemuldiv2  12120  ltdiv2  12125  lediv2  12129  infrelb  12224  nndivtr  12307  bndndx  12527  nn0n0n1ge2  12596  fnn0ind  12720  addlelt  13158  xrletr  13209  qsqueeze  13253  xleadd2a  13306  xleadd1  13307  xltadd2  13309  xltmul2  13345  supxrbnd  13380  iooneg  13524  iccneg  13525  icoshft  13526  icoshftf1o  13527  zltaddlt1le  13558  fzen  13595  uzsubsubfz  13601  ssfzunsnext  13624  fzrevral2  13668  fzshftral  13670  fz0fzdiffz0  13692  elfzmlbp  13694  elfzo  13716  nelfzo  13720  fzoaddel2  13776  fzosubel2  13781  ssfzo12bi  13817  fzonfzoufzol  13827  subfzo0  13849  flltdivnn0lt  13894  modmulnn  13950  modcyc  13967  modaddabs  13972  modaddmod  13973  modmuladd  13977  modadd2mod  13985  modsubmod  13993  modsubmodmod  13994  modaddmodup  13998  modmulmod  14000  modsubdir  14004  modfzo0difsn  14007  modsumfzodifsn  14008  uzindi  14046  axdc4uzlem  14047  expneg2  14134  expdiv  14177  expubnd  14242  mulbinom2  14287  bernneq2  14294  expnngt1  14305  hashinfxadd  14449  hashunsngx  14457  hashunsnggt  14458  hashfundm  14507  hashf1dmcdm  14509  hashdifsnp1  14571  ccatval3  14644  ccatfv0  14649  ccatval1lsw  14650  ccats1val2  14695  ccatw2s1p1  14704  swrdnd  14724  pfxsuffeqwrdeq  14767  pfxsuff1eqwrdeq  14768  swrdswrd  14774  pfxpfx  14777  wrd2ind  14792  swrdccatin1  14794  pfxccatin12lem1  14797  swrdccatin2  14798  pfxccatin12lem3  14801  swrdccat  14804  pfxccatpfx1  14805  pfxccatpfx2  14806  swrdccat3blem  14808  swrdrevpfx  14838  repswswrd  14855  repswpfx  14856  repswccat  14857  cshwidxmod  14874  2cshw  14884  3cshw  14889  scshwfzeqfzo  14897  cshwcsh2id  14899  cshimadifsn  14900  cshimadifsn0  14901  ccatco  14906  cshco  14907  swrdco  14908  pfxco  14909  lswco  14910  swrds2  15011  2swrd2eqwrdeq  15026  shftuz  15142  sgn3da  15174  abs3dif  15419  fsumdifsnconst  15878  modfsummods  15880  sin02gt0  16280  dvdsval2  16345  dvdscmul  16372  dvdsmulc  16373  dvdscmulr  16374  dvdsmulcr  16375  divalglem8  16490  ndvdssub  16499  dvdsexpim  16645  rpmulgcd  16647  expgcd  16653  zexpgcd  16655  coprmprod  16751  cncongr1  16757  cncongr2  16758  isprm3  16773  modprm0  16897  coprimeprodsq  16900  pythagtriplem12  16918  pythagtriplem14  16920  pcprendvds  16932  pcmul  16943  pcdiv  16944  pcqcl  16948  pcqdiv  16949  pcdvdsb  16961  vdwnnlem1  17087  hashbcss  17096  cshwshashlem1  17187  fvsetsid  17260  setsstruct2  17266  setsstruct  17268  mrcss  17704  mrcsscl  17708  mrcun  17710  cofulid  17979  catcisolem  18199  funcsetcestrclem9  18251  latleeqj1  18539  lubun  18603  clatleglb  18606  pslem  18660  dirtr  18690  mgmb1mgm1  18747  pwspjmhm  18939  grpinvid1  19115  grpinvid2  19116  grpasscan1  19125  grpasscan2  19126  grpinvadd  19141  grpsubf  19142  grpsubrcan  19144  grpinvsub  19145  grpsubeq0  19149  grpsubadd0sub  19150  grppncan  19154  grpnpcan  19155  mulgnn0p1  19208  mulgaddcomlem  19220  mulginvcom  19222  mulginvinv  19223  subgsubcl  19261  subgsub  19262  eqglact  19304  qussub  19319  ghmsub  19351  psgnunilem4  19624  oddvds2  19693  odsubdvds  19698  gexnnod  19715  slwn0  19742  dvrcl  20545  unitdvcl  20546  dvrcan1  20550  dvrcan3  20551  dvreq1  20552  rngisom1  20607  rngisomring  20608  subrgdv  20751  isdrng3lem2  20915  abvsubtri  20993  idsrngd  21022  lmodvsubval2  21101  lsmcl  21267  lsmsp2  21271  lspsntrim  21282  rngqiprngimfolem  21493  lidldvgen  21565  cncrng  21606  chrcong  21740  dvdschrmulg  21741  zndvds  21762  zntoslem  21769  ocvsscon  21888  obselocv  21941  frlmphl  21994  ascldimul  22103  mpfsubrg  22327  ply1tmcl  22498  eqcoe1ply1eq  22524  gsummoncoe1  22533  lply1binomsc  22536  mamudm  22617  mamufacex  22618  scmatf1  22753  scmatf1o  22754  scmatrngiso  22758  submabas  22800  mdetdiaglem  22820  mdetralt2  22831  mdetero  22832  mdetunilem2  22835  mdetunilem6  22839  m2detleiblem7  22849  maducoeval2  22862  gsummatr01lem3  22879  gsummatr01  22881  smadiadetglem2  22894  matunitlindflem1  22901  cramerlem1  22912  mply1topmatcl  23030  mp2pm2mplem4  23034  ntrin  23286  elnei  23336  neindisj2  23348  ordtopn3  23421  leordtval2  23437  lecldbas  23444  cnrest2  23511  cmpsublem  23624  ptrescn  23865  xkococn  23886  kqfeq  23950  snfbas  24092  neifil  24106  fclsrest  24250  utopsnnei  24475  neipcfilu  24521  psmetsym  24536  psmetge0  24538  xmetge0  24570  xmetsym  24573  metustto  24779  metustbl  24792  restmetu  24796  nm2dif  24851  nmtri  24852  cnmet  24997  cnmpopc  25156  iihalf1  25159  iihalf2  25161  iocopnst  25168  clmnegsubdi2  25333  clmsub4  25334  clmvsubval2  25338  ncvspi  25384  cphsqrtcl3  25415  cph2ass  25441  cphipval2  25469  cphipval  25471  caublcls  25537  bcthlem3  25554  bcthlem4  25555  srabn  25588  cssbn  25603  cmslsschl  25605  rrxmet  25636  rrxdsfi  25639  iblconst  26045  dvdsq1p  26388  coeid3  26466  aannenlem2  26565  pserdvlem2  26664  tanord1  26774  cxpef  26902  recxpcl  26912  logbchbase  27008  relogbcl  27010  relogbzcl  27011  logbleb  27020  logblt  27021  relogbcxpb  27024  lawcos  27053  pythag  27054  isosctrlem1  27055  isosctrlem2  27056  lgsmodeq  27578  lgsmulsqcoprm  27579  gausslemma2dlem1a  27601  2lgsoddprmlem2  27645  ltsres  27898  lestr  27998  cofcutr  28189  lrrecpo  28206  ltadds2im  28251  leadds2im  28253  leadds1  28254  leadds2  28255  ltadds1  28257  addscan2  28258  addscan1  28259  ltsubs1  28341  divmulsw  28458  oldfib  28642  zsoring  28674  bdayfinbndlem1  28732  ax5seglem1  29385  axcontlem2  29422  axcontlem8  29428  upgrpredgv  29596  numedglnl  29601  issubgr2  29732  uhgrissubgr  29735  egrsubgr  29737  nbusgrfi  29834  nb3grprlem2  29841  cplgr3v  29895  cusgrsizeindslem  29911  finsumvtxdg2size  30010  rusgrpropadjvtx  30045  upgrwlkvtxedg  30104  swrdwlk  30147  usgr2trlncl  30225  uspgrn2crct  30276  crctcshwlkn0lem4  30281  crctcshwlkn0lem5  30282  wwlksnextproplem3  30379  umgr2adedgwlklem  30412  rusgr0edg  30444  clwwlk1loop  30458  clwwlkccatlem  30459  clwlkclwwlklem2a4  30467  clwlkclwwlklem2a  30468  clwwisshclwwslemlem  30483  erclwwlktr  30492  clwwlkel  30516  erclwwlkntr  30541  clwwlknonex2lem2  30578  uhgr3cyclex  30662  umgr3cyclex  30663  eucrctshift  30723  frgr3v  30755  3cyclfrgrrn  30766  frgrwopreglem5a  30791  frgr2wsp1  30810  extwwlkfab  30832  clwwlknonclwlknonf1o  30842  numclwwlk3lem1  30862  numclwwlk5  30868  numclwwlk6  30870  isgrpo  30978  grpoinvid1  31009  grpoinvid2  31010  grpoinvop  31014  grpodivinv  31017  grpoinvdiv  31018  grpodivf  31019  grponpcan  31024  ablonncan  31037  nvmval  31123  nvmval2  31124  nvmfval  31125  nvmul0or  31131  nvpncan2  31134  nvaddsub4  31138  nvmeq0  31139  nvdif  31147  nvpi  31148  nvmtri  31152  nvabs  31153  imsmetlem  31171  ipval2lem3  31186  ipval2  31188  4ipval2  31189  ipval3  31190  nmooge0  31248  blometi  31284  hvaddsub12  31519  hvsubdistr1  31530  hvsubdistr2  31531  hvaddcan2  31552  hvmulcan  31553  hvmulcan2  31554  hvsubcan  31555  hvsubcan2  31556  his7  31571  his2sub  31573  his2sub2  31574  norm3dif2  31632  shsubcl  31701  hhssnv  31745  shlej2  31842  fh2  32100  cm2j  32101  pjoi0  32198  hodcl  32228  hosubdi  32289  unopf1o  32397  unopadj  32400  adj2  32415  braadd  32426  bramul  32427  lnopaddmuli  32454  lnopsubmuli  32456  homco2  32458  lnfnaddmuli  32526  adjlnop  32567  leopmul  32615  leoptr  32618  pjimai  32657  atcv1  32861  atexch  32862  atcvatlem  32866  fcoinvbr  33078  preiman0  33182  divnumden2  33286  xdivmul  33370  cshf1o  33402  resvsca  33772  idlsrgcmnd  33925  hasheuni  34595  cndprobin  34945  bayesth  34950  signstfvp  35079  breprexplemc  35140  trssfir1om  35621  fineqvac  35642  fineqvnttrclselem1  35647  fineqvnttrclselem3  35649  trssfir1omregs  35662  lediv2aALT  36256  fununiq  36348  dfrdg2  36372  clsun  36947  neiin  36951  rdgeqoa  38124  poimirlem32  38401  ftc1anclem4  38445  areacirc  38462  filbcmb  38490  ismtybnd  38557  grpoeqdivid  38631  ghomco  38641  rngonegrmul  38694  zerdivemp1x  38697  rngohomco  38724  rngoisoco  38732  riscer  38738  intidl  38779  isfldidl  38818  eceldmqsxrncnvepres  39184  eceldmqsxrncnvepres2  39185  brredunds  39458  lshpnelb  39857  opnlen0  40061  opcon3b  40069  opcon2b  40070  oplecon3b  40073  opltcon3b  40077  opltcon2b  40079  oldmm1  40090  oldmm4  40093  oldmj1  40094  oldmj4  40097  cvrval2  40147  cvrcon3b  40150  leatb  40165  atcmp  40184  atcvreq0  40187  atlatle  40193  athgt  40329  3dim2  40341  islln2a  40390  lplnnleat  40415  lvolnleat  40456  4atlem10  40479  4atlem11  40482  4atlem12  40485  dalem21  40567  dalem22  40568  dalem23  40569  dalem29  40574  dalem30  40575  dalem31N  40576  dalem32  40577  dalem33  40578  dalem34  40579  dalem35  40580  dalem36  40581  dalem37  40582  dalem40  40585  dalem46  40591  dalem47  40592  dalem51  40596  dalem52  40597  dalem58  40603  dalem59  40604  pmaple  40634  paddclN  40715  pmapjoin  40725  pmapjat1  40726  elpcliN  40766  pclssN  40767  pclun2N  40772  2polcon4bN  40791  paddunN  40800  poldmj1N  40801  pmapj2N  40802  pmapocjN  40803  psubclinN  40821  paddatclN  40822  poml4N  40826  lautco  40970  ldilco  40989  ltrneq2  41021  trljat1  41039  cdlemc1  41064  cdleme10  41127  ltrnco  41592  trlcocnv  41593  trljco  41613  trljco2  41614  cdlemi1  41691  tendocnv  41894  diaord  41920  dibord  42032  dihord3  42130  dihord4  42131  dihmeetlem2N  42172  dihmeetlem4preN  42179  dochdmj1  42263  hdmap10lem  42712  lcmineqlem1  42895  sticksstones2  43013  readdsub  43259  reltsub1  43261  renpncan3  43266  reppncan  43268  resubdi  43271  readdcan2  43288  mzprename  43594  dvdsrabdioph  43651  pell14qrdivcl  43706  monotoddzz  43784  jm2.19lem2  43831  jm2.19  43834  relexpaddss  44558  k0004lem3  44989  dvconstbi  45158  chordthmALT  45755  isosctrlem1ALT  45756  ssinc  45919  ssdec  45920  wessf1ornlem  46017  disjf1o  46023  ssnnf1octb  46026  projf1o  46028  mapssbi  46043  iunmapsn  46047  upbdrech  46138  iuneqfzuzlem  46164  suplesup  46169  rexabslelem  46246  climxrrelem  46577  limsupresxr  46594  liminfresxr  46595  liminfvalxr  46611  xlimliminflimsup  46690  cncfshift  46702  cncfperiod  46707  cncfuni  46714  icccncfext  46715  dvmptfprodlem  46772  dvnprodlem1  46774  itgspltprt  46807  ismbl3  46814  stoweidlem3  46831  stoweidlem10  46838  stoweidlem19  46847  stoweidlem31  46859  stoweidlem34  46862  stoweidlem44  46872  fourierdlem41  46976  fourierdlem42  46977  fourierdlem51  46985  fourierdlem68  47002  fourierdlem89  47023  fourierdlem91  47025  fourierdlem92  47026  fourierdlem94  47028  etransclem24  47086  etransclem34  47096  qndenserrnbllem  47122  salincl  47152  saldifcl2  47156  subsalsal  47187  sge0pr  47222  sge0pnffigt  47224  sge0reuz  47275  nnfoctbdjlem  47283  nnfoctbdj  47284  meadjiunlem  47293  caratheodorylem2  47355  hoidmv1le  47422  hoidmvlelem3  47425  hspmbllem2  47455  opnvonmbllem2  47461  smfaddlem1  47591  sigaraf  47681  sigarmf  47682  nltle2tri  48201  subsubelfzo0  48215  nnmul2  48218  submodaddmod  48235  zplusmodne  48237  addmodne  48238  minusmod5ne  48243  submodneaddmod  48245  modmkpkne  48255  modmknepk  48256  iccpartiltu  48322  icceuelpart  48336  poprelb  48424  reuopreuprim  48426  nprmmul2  48428  proththd  48517  mogoldbblem  48636  fppr2odd  48647  fpprel2  48657  bgoldbtbndlem2  48722  clnbusgrfi  48759  grimuhgr  48803  uhgrimisgrgric  48847  clnbgrgrim  48850  grtrif1o  48858  grlimgrtri  48919  gpgusgralem  48972  gpgedgvtx0  48977  gpgedg2ov  48982  gpgedg2iv  48983  gpg5nbgrvtx03starlem2  48985  nn0sumltlt  49280  invginvrid  49297  ply1sclrmsm  49314  linccl  49344  lincvalpr  49348  lincresunit3lem1  49409  lincresunit3  49411  fdivmpt  49470  nnolog2flm1  49520  dignnld  49533  digexp  49537  dignn0flhalflem1  49545  itcovalsucov  49598  reorelicc  49640  eenglngeehlnmlem1  49667  line2  49682  line2xlem  49683  itsclc0lem1  49686  itsclc0xyqsolr  49699  i0oii  49846  io1ii  49847  indthinc  50388  indthincALT  50389  setrec2fun  50618  reccot  50684  rectan  50685