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  3663  onunel  6470  iotan0OLD  6529  fununiq  6556  funopg  6575  dff1o2  6831  fvelimad  6953  unima  6961  fnimapr  6969  fvmptt  7015  fnreseql  7048  xpprsng  7143  xpsnprg  7144  f1elima  7268  f1ounsn  7281  f13dfv  7283  f1ocnvfvb  7288  f1cdmsn  7291  f1ofvswap  7315  oprssov  7591  resf1extb  7947  resf1ext2b  7948  funelss  8059  poxp  8143  poxp2  8163  poxp3  8170  smoiso  8374  oaord  8559  oaword  8561  omcan  8581  omwordri  8584  odi  8591  omeulem1  8594  oeord  8601  oecan  8602  oewordri  8605  oeordsuc  8607  nnaord  8632  nnaordr  8633  nndi  8636  nnaword  8640  nnmwordri  8649  naddel2  8702  naddss1  8703  naddss2  8704  erov  8839  ecopovtrn  8845  curfv  8896  mapsnd  8918  f1dom3g  8998  xpdom3  9098  mapxpen  9166  dif1en  9181  findcard  9183  f1domfi2  9201  entrfir  9210  domtrfil  9211  domtrfir  9213  sbthfilem  9217  sdomdomtrfi  9220  php3  9228  findcard3  9278  indexfi  9353  suppr  9468  infpr  9501  r111  9786  tcrank  9905  setrec2fun  9977  acndom  10134  infdif2  10291  infxpdom  10292  cfeq0  10338  cfsuc  10339  cfflb  10341  cflim2  10345  cfsmolem  10352  axcc3  10520  domtriomlem  10524  axdc3lem2  10533  axdc3lem4  10535  axdc4lem  10537  axcclem  10539  pwcfsdom  10672  tsktrss  10850  tsksuc  10851  tskuni  10872  adderpqlem  11043  mulerpqlem  11044  mulcanenq  11049  distrnq  11050  ltsonq  11058  ltanq  11060  ltmnq  11061  distrlem1pr  11114  distrlem5pr  11116  ltsopr  11121  ltsosr  11183  ltasr  11189  adddir  11301  axlttrn  11386  nnncan1  11598  npncan3  11600  pnpcan2  11602  subdi  11753  subdir  11754  mulcan1g  11973  mulcan2g  11974  divmul  11981  div23  11997  div13  11999  muldivdir  12013  divsubdir  12014  subdivcomb1  12016  divcan7  12030  ltmul2  12172  lemul1  12173  lemul2  12174  lemul2a  12176  lediv1  12186  ltmuldiv2  12195  lemuldiv  12201  lemuldiv2  12202  ltdiv2  12207  lediv2  12211  infrelb  12306  nndivtr  12389  bndndx  12609  nn0n0n1ge2  12678  fnn0ind  12802  addlelt  13240  xrletr  13291  qsqueeze  13335  xleadd2a  13388  xleadd1  13389  xltadd2  13391  xltmul2  13427  supxrbnd  13462  iooneg  13606  iccneg  13607  icoshft  13608  icoshftf1o  13609  zltaddlt1le  13640  fzen  13678  uzsubsubfz  13684  ssfzunsnext  13707  fzrevral2  13751  fzshftral  13753  fz0fzdiffz0  13775  elfzmlbp  13777  elfzo  13799  nelfzo  13803  fzoaddel2  13859  fzosubel2  13864  ssfzo12bi  13900  fzonfzoufzol  13910  subfzo0  13932  flltdivnn0lt  13977  modmulnn  14033  modcyc  14050  modaddabs  14055  modaddmod  14056  modmuladd  14060  modadd2mod  14068  modsubmod  14076  modsubmodmod  14077  modaddmodup  14081  modmulmod  14083  modsubdir  14087  modfzo0difsn  14090  modsumfzodifsn  14091  uzindi  14129  axdc4uzlem  14130  expneg2  14217  expdiv  14260  expubnd  14325  mulbinom2  14371  bernneq2  14378  expnngt1  14389  hashinfxadd  14533  hashunsngx  14541  hashunsnggt  14542  hashfundm  14591  hashf1dmcdm  14593  hashdifsnp1  14655  ccatval3  14728  ccatfv0  14733  ccatval1lsw  14734  ccats1val2  14780  ccatw2s1p1  14789  swrdnd  14809  pfxsuffeqwrdeq  14852  pfxsuff1eqwrdeq  14853  swrdswrd  14859  pfxpfx  14862  wrd2ind  14877  swrdccatin1  14879  pfxccatin12lem1  14882  swrdccatin2  14883  pfxccatin12lem3  14886  swrdccat  14889  pfxccatpfx1  14890  pfxccatpfx2  14891  swrdccat3blem  14893  swrdrevpfx  14923  repswswrd  14940  repswpfx  14941  repswccat  14942  cshwidxmod  14959  2cshw  14969  3cshw  14974  scshwfzeqfzo  14982  cshwcsh2id  14984  cshimadifsn  14985  cshimadifsn0  14986  ccatco  14991  cshco  14992  swrdco  14993  pfxco  14994  lswco  14995  swrds2  15097  2swrd2eqwrdeq  15112  shftuz  15228  sgn3da  15260  abs3dif  15505  fsumdifsnconst  15964  modfsummods  15966  sin02gt0  16366  dvdsval2  16431  dvdscmul  16458  dvdsmulc  16459  dvdscmulr  16460  dvdsmulcr  16461  divalglem8  16576  ndvdssub  16585  dvdsexpim  16734  rpmulgcd  16737  expgcd  16743  zexpgcd  16745  coprmprod  16842  cncongr1  16848  cncongr2  16849  isprm3  16864  modprm0  16989  coprimeprodsq  16992  pythagtriplem12  17010  pythagtriplem14  17012  pcprendvds  17024  pcmul  17035  pcdiv  17036  pcqcl  17040  pcqdiv  17041  pcdvdsb  17053  vdwnnlem1  17179  hashbcss  17188  cshwshashlem1  17279  fvsetsid  17352  setsstruct2  17358  setsstruct  17360  mrcss  17796  mrcsscl  17800  mrcun  17802  cofulid  18071  catcisolem  18291  funcsetcestrclem9  18343  latleeqj1  18631  lubun  18695  clatleglb  18698  pslem  18752  dirtr  18782  mgmb1mgm1  18839  pwspjmhm  19032  grpinvid1  19208  grpinvid2  19209  grpasscan1  19218  grpasscan2  19219  grpinvadd  19234  grpsubf  19235  grpsubrcan  19237  grpinvsub  19238  grpsubeq0  19242  grpsubadd0sub  19243  grppncan  19247  grpnpcan  19248  mulgnn0p1  19301  mulgaddcomlem  19313  mulginvcom  19315  mulginvinv  19316  subgsubcl  19354  subgsub  19355  eqglact  19397  qussub  19412  ghmsub  19444  psgnunilem4  19717  oddvds2  19786  odsubdvds  19791  gexnnod  19808  slwn0  19835  dvrcl  20640  unitdvcl  20641  dvrcan1  20645  dvrcan3  20646  dvreq1  20647  rngisom1  20702  rngisomring  20703  subrgdv  20847  isdrng3lem2  21012  abvsubtri  21090  idsrngd  21119  lmodvsubval2  21198  lsmcl  21364  lsmsp2  21368  lspsntrim  21379  rngqiprngimfolem  21592  lidldvgen  21664  cncrng  21705  chrcong  21839  dvdschrmulg  21840  zndvds  21861  zntoslem  21868  ocvsscon  21987  obselocv  22040  frlmphl  22093  ascldimul  22202  mpfsubrg  22426  ply1tmcl  22597  eqcoe1ply1eq  22623  gsummoncoe1  22632  lply1binomsc  22635  mamudm  22716  mamufacex  22717  scmatf1  22852  scmatf1o  22853  scmatrngiso  22857  submabas  22899  mdetdiaglem  22919  mdetralt2  22930  mdetero  22931  mdetunilem2  22934  mdetunilem6  22938  m2detleiblem7  22948  maducoeval2  22961  gsummatr01lem3  22978  gsummatr01  22980  smadiadetglem2  22993  matunitlindflem1  23000  cramerlem1  23011  mply1topmatcl  23129  mp2pm2mplem4  23133  ntrin  23385  elnei  23435  neindisj2  23447  ordtopn3  23520  leordtval2  23536  lecldbas  23543  cnrest2  23610  cmpsublem  23723  ptrescn  23964  xkococn  23985  kqfeq  24049  snfbas  24191  neifil  24205  fclsrest  24349  utopsnnei  24574  neipcfilu  24620  psmetsym  24635  psmetge0  24637  xmetge0  24669  xmetsym  24672  metustto  24878  metustbl  24891  restmetu  24895  nm2dif  24950  nmtri  24951  cnmet  25096  cnmpopc  25255  iihalf1  25258  iihalf2  25260  iocopnst  25267  clmnegsubdi2  25432  clmsub4  25433  clmvsubval2  25437  ncvspi  25483  cphsqrtcl3  25514  cph2ass  25540  cphipval2  25568  cphipval  25570  caublcls  25636  bcthlem3  25653  bcthlem4  25654  srabn  25687  cssbn  25702  cmslsschl  25704  rrxmet  25735  rrxdsfi  25738  iblconst  26144  dvdsq1p  26487  coeid3  26565  aannenlem2  26662  pserdvlem2  26761  tanord1  26871  cxpef  26999  recxpcl  27009  logbchbase  27105  relogbcl  27107  relogbzcl  27108  logbleb  27117  logblt  27118  relogbcxpb  27121  lawcos  27150  pythag  27151  isosctrlem1  27152  isosctrlem2  27153  lgsmodeq  27675  lgsmulsqcoprm  27676  gausslemma2dlem1a  27698  2lgsoddprmlem2  27742  ltsres  28025  lestr  28125  cofcutr  28316  lrrecpo  28333  ltadds2im  28378  leadds2im  28380  leadds1  28381  leadds2  28382  ltadds1  28384  addscan2  28385  addscan1  28386  ltsubs1  28468  divmulsw  28585  oldfib  28769  zsoring  28801  bdayfinbndlem1  28859  ax5seglem1  29512  axcontlem2  29549  axcontlem8  29555  upgrpredgv  29723  numedglnl  29728  issubgr2  29859  uhgrissubgr  29862  egrsubgr  29864  nbusgrfi  29961  nb3grprlem2  29968  cplgr3v  30022  cusgrsizeindslem  30038  finsumvtxdg2size  30137  rusgrpropadjvtx  30172  upgrwlkvtxedg  30231  swrdwlk  30274  usgr2trlncl  30352  uspgrn2crct  30403  crctcshwlkn0lem4  30408  crctcshwlkn0lem5  30409  wwlksnextproplem3  30506  umgr2adedgwlklem  30539  rusgr0edg  30571  clwwlk1loop  30585  clwwlkccatlem  30586  clwlkclwwlklem2a4  30594  clwlkclwwlklem2a  30595  clwwisshclwwslemlem  30610  erclwwlktr  30619  clwwlkel  30643  erclwwlkntr  30668  clwwlknonex2lem2  30705  uhgr3cyclex  30789  umgr3cyclex  30790  eucrctshift  30850  frgr3v  30882  3cyclfrgrrn  30893  frgrwopreglem5a  30918  frgr2wsp1  30937  extwwlkfab  30959  clwwlknonclwlknonf1o  30969  numclwwlk3lem1  30989  numclwwlk5  30995  numclwwlk6  30997  isgrpo  31105  grpoinvid1  31136  grpoinvid2  31137  grpoinvop  31141  grpodivinv  31144  grpoinvdiv  31145  grpodivf  31146  grponpcan  31151  ablonncan  31164  nvmval  31250  nvmval2  31251  nvmfval  31252  nvmul0or  31258  nvpncan2  31261  nvaddsub4  31265  nvmeq0  31266  nvdif  31274  nvpi  31275  nvmtri  31279  nvabs  31280  imsmetlem  31298  ipval2lem3  31313  ipval2  31315  4ipval2  31316  ipval3  31317  nmooge0  31375  blometi  31411  hvaddsub12  31646  hvsubdistr1  31657  hvsubdistr2  31658  hvaddcan2  31679  hvmulcan  31680  hvmulcan2  31681  hvsubcan  31682  hvsubcan2  31683  his7  31698  his2sub  31700  his2sub2  31701  norm3dif2  31759  shsubcl  31828  hhssnv  31872  shlej2  31969  fh2  32227  cm2j  32228  pjoi0  32325  hodcl  32355  hosubdi  32416  unopf1o  32524  unopadj  32527  adj2  32542  braadd  32553  bramul  32554  lnopaddmuli  32581  lnopsubmuli  32583  homco2  32585  lnfnaddmuli  32653  adjlnop  32694  leopmul  32742  leoptr  32745  pjimai  32784  atcv1  32988  atexch  32989  atcvatlem  32993  fcoinvbr  33247  preiman0  33351  divnumden2  33454  xdivmul  33538  cshf1o  33570  resvsca  33940  idlsrgcmnd  34094  hasheuni  34764  cndprobin  35113  bayesth  35118  signstfvp  35247  breprexplemc  35308  f1preimaex  35762  trssfir1om  35790  acwer1prclem  35816  fineqvac  35841  fineqvnttrclselem1  35846  fineqvnttrclselem3  35848  trssfir1omregs  35861  lediv2aALT  36529  dfrdg2  36650  clsun  37209  neiin  37213  rdgeqoa  38387  poimirlem32  38664  ftc1anclem4  38708  areacirc  38725  filbcmb  38768  ismtybnd  38835  grpoeqdivid  38909  ghomco  38919  rngonegrmul  38972  zerdivemp1x  38975  rngohomco  39002  rngoisoco  39010  riscer  39016  intidl  39057  isfldidl  39096  eceldmqsxrncnvepres  39462  eceldmqsxrncnvepres2  39463  brredunds  39736  lshpnelb  40135  opnlen0  40339  opcon3b  40347  opcon2b  40348  oplecon3b  40351  opltcon3b  40355  opltcon2b  40357  oldmm1  40368  oldmm4  40371  oldmj1  40372  oldmj4  40375  cvrval2  40425  cvrcon3b  40428  leatb  40443  atcmp  40462  atcvreq0  40465  atlatle  40471  athgt  40607  3dim2  40619  islln2a  40668  lplnnleat  40693  lvolnleat  40734  4atlem10  40757  4atlem11  40760  4atlem12  40763  dalem21  40845  dalem22  40846  dalem23  40847  dalem29  40852  dalem30  40853  dalem31N  40854  dalem32  40855  dalem33  40856  dalem34  40857  dalem35  40858  dalem36  40859  dalem37  40860  dalem40  40863  dalem46  40869  dalem47  40870  dalem51  40874  dalem52  40875  dalem58  40881  dalem59  40882  pmaple  40912  paddclN  40993  pmapjoin  41003  pmapjat1  41004  elpcliN  41044  pclssN  41045  pclun2N  41050  2polcon4bN  41069  paddunN  41078  poldmj1N  41079  pmapj2N  41080  pmapocjN  41081  psubclinN  41099  paddatclN  41100  poml4N  41104  lautco  41248  ldilco  41267  ltrneq2  41299  trljat1  41317  cdlemc1  41342  cdleme10  41405  ltrnco  41870  trlcocnv  41871  trljco  41891  trljco2  41892  cdlemi1  41969  tendocnv  42172  diaord  42198  dibord  42310  dihord3  42408  dihord4  42409  dihmeetlem2N  42450  dihmeetlem4preN  42457  dochdmj1  42541  hdmap10lem  42990  lcmineqlem1  43173  sticksstones2  43291  readdsub  43529  reltsub1  43531  renpncan3  43536  reppncan  43538  resubdi  43541  readdcan2  43558  mzprename  43854  dvdsrabdioph  43911  pell14qrdivcl  43966  monotoddzz  44044  jm2.19lem2  44091  jm2.19  44094  relexpaddss  44812  k0004lem3  45243  dvconstbi  45412  chordthmALT  46009  isosctrlem1ALT  46010  ssinc  46196  ssdec  46197  wessf1ornlem  46294  disjf1o  46300  ssnnf1octb  46303  projf1o  46305  mapssbi  46320  iunmapsn  46324  upbdrech  46415  iuneqfzuzlem  46440  suplesup  46445  rexabslelem  46522  climxrrelem  46853  limsupresxr  46870  liminfresxr  46871  liminfvalxr  46887  xlimliminflimsup  46966  cncfshift  46978  cncfperiod  46983  cncfuni  46990  icccncfext  46991  dvmptfprodlem  47048  dvnprodlem1  47050  itgspltprt  47083  ismbl3  47090  stoweidlem3  47107  stoweidlem10  47114  stoweidlem19  47123  stoweidlem31  47135  stoweidlem34  47138  stoweidlem44  47148  fourierdlem41  47252  fourierdlem42  47253  fourierdlem51  47261  fourierdlem68  47278  fourierdlem89  47299  fourierdlem91  47301  fourierdlem92  47302  fourierdlem94  47304  etransclem24  47362  etransclem34  47372  qndenserrnbllem  47398  salincl  47428  saldifcl2  47432  subsalsal  47463  sge0pr  47498  sge0pnffigt  47500  sge0reuz  47551  nnfoctbdjlem  47559  nnfoctbdj  47560  meadjiunlem  47569  caratheodorylem2  47631  hoidmv1le  47698  hoidmvlelem3  47701  hspmbllem2  47731  opnvonmbllem2  47737  smfaddlem1  47867  sigaraf  47957  sigarmf  47958  nltle2tri  48477  subsubelfzo0  48491  nnmul2  48494  submodaddmod  48511  zplusmodne  48513  addmodne  48514  minusmod5ne  48519  submodneaddmod  48521  modmkpkne  48531  modmknepk  48532  iccpartiltu  48598  icceuelpart  48612  poprelb  48700  reuopreuprim  48702  nprmmul2  48704  proththd  48793  mogoldbblem  48912  fppr2odd  48923  fpprel2  48933  bgoldbtbndlem2  48998  clnbusgrfi  49035  grimuhgr  49079  uhgrimisgrgric  49123  clnbgrgrim  49126  grtrif1o  49134  grlimgrtri  49195  gpgusgralem  49248  gpgedgvtx0  49253  gpgedg2ov  49258  gpgedg2iv  49259  gpg5nbgrvtx03starlem2  49261  nn0sumltlt  49556  invginvrid  49573  ply1sclrmsm  49590  linccl  49620  lincvalpr  49624  lincresunit3lem1  49685  lincresunit3  49687  fdivmpt  49746  nnolog2flm1  49796  dignnld  49809  digexp  49813  dignn0flhalflem1  49821  itcovalsucov  49874  reorelicc  49916  eenglngeehlnmlem1  49944  line2  49958  line2xlem  49959  itsclc0lem1  49962  itsclc0xyqsolr  49975  i0oii  50128  io1ii  50129  indthinc  50691  indthincALT  50692  reccot  51020  rectan  51021