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  2661  eqeu  3664  onunel  6469  iotan0  6527  funopg  6572  dff1o2  6828  fvelimad  6950  unima  6958  fnimapr  6966  fvmptt  7012  fnreseql  7045  xpprsng  7140  xpsnprg  7141  f1elima  7265  f1ounsn  7278  f13dfv  7280  f1ocnvfvb  7285  f1cdmsn  7288  f1ofvswap  7312  oprssov  7588  resf1extb  7944  resf1ext2b  7945  funelss  8056  poxp  8138  poxp2  8153  poxp3  8160  smoiso  8363  oaord  8548  oaword  8550  omcan  8570  omwordri  8573  odi  8580  omeulem1  8583  oeord  8590  oecan  8591  oewordri  8594  oeordsuc  8596  nnaord  8621  nnaordr  8622  nndi  8625  nnaword  8629  nnmwordri  8638  naddel2  8691  naddss1  8692  naddss2  8693  erov  8828  ecopovtrn  8834  curfv  8885  mapsnd  8907  f1dom3g  8987  xpdom3  9087  mapxpen  9155  dif1en  9170  findcard  9172  f1domfi2  9190  entrfir  9199  domtrfil  9200  domtrfir  9202  sbthfilem  9206  sdomdomtrfi  9209  php3  9217  findcard3  9267  indexfi  9342  suppr  9457  infpr  9490  r111  9775  tcrank  9894  setrec2fun  9966  acndom  10123  infdif2  10280  infxpdom  10281  cfeq0  10327  cfsuc  10328  cfflb  10330  cflim2  10334  cfsmolem  10341  axcc3  10509  domtriomlem  10513  axdc3lem2  10522  axdc3lem4  10524  axdc4lem  10526  axcclem  10528  pwcfsdom  10661  tsktrss  10839  tsksuc  10840  tskuni  10861  adderpqlem  11032  mulerpqlem  11033  mulcanenq  11038  distrnq  11039  ltsonq  11047  ltanq  11049  ltmnq  11050  distrlem1pr  11103  distrlem5pr  11105  ltsopr  11110  ltsosr  11172  ltasr  11178  adddir  11290  axlttrn  11375  letr  11397  nnncan1  11587  npncan3  11589  pnpcan2  11591  subdi  11742  subdir  11743  mulcan1g  11962  mulcan2g  11963  divmul  11970  div23  11986  div13  11988  muldivdir  12002  divsubdir  12003  subdivcomb1  12005  divcan7  12019  ltmul2  12161  lemul1  12162  lemul2  12163  lemul2a  12165  lediv1  12175  ltmuldiv2  12184  lemuldiv  12190  lemuldiv2  12191  ltdiv2  12196  lediv2  12200  infrelb  12295  nndivtr  12378  bndndx  12598  nn0n0n1ge2  12667  fnn0ind  12791  addlelt  13229  xrletr  13280  qsqueeze  13324  xleadd2a  13377  xleadd1  13378  xltadd2  13380  xltmul2  13416  supxrbnd  13451  iooneg  13595  iccneg  13596  icoshft  13597  icoshftf1o  13598  zltaddlt1le  13629  fzen  13667  uzsubsubfz  13673  ssfzunsnext  13696  fzrevral2  13740  fzshftral  13742  fz0fzdiffz0  13764  elfzmlbp  13766  elfzo  13788  nelfzo  13792  fzoaddel2  13848  fzosubel2  13853  ssfzo12bi  13889  fzonfzoufzol  13899  subfzo0  13921  flltdivnn0lt  13966  modmulnn  14022  modcyc  14039  modaddabs  14044  modaddmod  14045  modmuladd  14049  modadd2mod  14057  modsubmod  14065  modsubmodmod  14066  modaddmodup  14070  modmulmod  14072  modsubdir  14076  modfzo0difsn  14079  modsumfzodifsn  14080  uzindi  14118  axdc4uzlem  14119  expneg2  14206  expdiv  14249  expubnd  14314  mulbinom2  14360  bernneq2  14367  expnngt1  14378  hashinfxadd  14522  hashunsngx  14530  hashunsnggt  14531  hashfundm  14580  hashf1dmcdm  14582  hashdifsnp1  14644  ccatval3  14717  ccatfv0  14722  ccatval1lsw  14723  ccats1val2  14768  ccatw2s1p1  14777  swrdnd  14797  pfxsuffeqwrdeq  14840  pfxsuff1eqwrdeq  14841  swrdswrd  14847  pfxpfx  14850  wrd2ind  14865  swrdccatin1  14867  pfxccatin12lem1  14870  swrdccatin2  14871  pfxccatin12lem3  14874  swrdccat  14877  pfxccatpfx1  14878  pfxccatpfx2  14879  swrdccat3blem  14881  swrdrevpfx  14911  repswswrd  14928  repswpfx  14929  repswccat  14930  cshwidxmod  14947  2cshw  14957  3cshw  14962  scshwfzeqfzo  14970  cshwcsh2id  14972  cshimadifsn  14973  cshimadifsn0  14974  ccatco  14979  cshco  14980  swrdco  14981  pfxco  14982  lswco  14983  swrds2  15084  2swrd2eqwrdeq  15099  shftuz  15215  sgn3da  15247  abs3dif  15492  fsumdifsnconst  15951  modfsummods  15953  sin02gt0  16353  dvdsval2  16418  dvdscmul  16445  dvdsmulc  16446  dvdscmulr  16447  dvdsmulcr  16448  divalglem8  16563  ndvdssub  16572  dvdsexpim  16721  rpmulgcd  16724  expgcd  16730  zexpgcd  16732  coprmprod  16829  cncongr1  16835  cncongr2  16836  isprm3  16851  modprm0  16976  coprimeprodsq  16979  pythagtriplem12  16997  pythagtriplem14  16999  pcprendvds  17011  pcmul  17022  pcdiv  17023  pcqcl  17027  pcqdiv  17028  pcdvdsb  17040  vdwnnlem1  17166  hashbcss  17175  cshwshashlem1  17266  fvsetsid  17339  setsstruct2  17345  setsstruct  17347  mrcss  17783  mrcsscl  17787  mrcun  17789  cofulid  18058  catcisolem  18278  funcsetcestrclem9  18330  latleeqj1  18618  lubun  18682  clatleglb  18685  pslem  18739  dirtr  18769  mgmb1mgm1  18826  pwspjmhm  19019  grpinvid1  19195  grpinvid2  19196  grpasscan1  19205  grpasscan2  19206  grpinvadd  19221  grpsubf  19222  grpsubrcan  19224  grpinvsub  19225  grpsubeq0  19229  grpsubadd0sub  19230  grppncan  19234  grpnpcan  19235  mulgnn0p1  19288  mulgaddcomlem  19300  mulginvcom  19302  mulginvinv  19303  subgsubcl  19341  subgsub  19342  eqglact  19384  qussub  19399  ghmsub  19431  psgnunilem4  19704  oddvds2  19773  odsubdvds  19778  gexnnod  19795  slwn0  19822  dvrcl  20627  unitdvcl  20628  dvrcan1  20632  dvrcan3  20633  dvreq1  20634  rngisom1  20689  rngisomring  20690  subrgdv  20834  isdrng3lem2  20999  abvsubtri  21077  idsrngd  21106  lmodvsubval2  21185  lsmcl  21351  lsmsp2  21355  lspsntrim  21366  rngqiprngimfolem  21579  lidldvgen  21651  cncrng  21692  chrcong  21826  dvdschrmulg  21827  zndvds  21848  zntoslem  21855  ocvsscon  21974  obselocv  22027  frlmphl  22080  ascldimul  22189  mpfsubrg  22413  ply1tmcl  22584  eqcoe1ply1eq  22610  gsummoncoe1  22619  lply1binomsc  22622  mamudm  22703  mamufacex  22704  scmatf1  22839  scmatf1o  22840  scmatrngiso  22844  submabas  22886  mdetdiaglem  22906  mdetralt2  22917  mdetero  22918  mdetunilem2  22921  mdetunilem6  22925  m2detleiblem7  22935  maducoeval2  22948  gsummatr01lem3  22965  gsummatr01  22967  smadiadetglem2  22980  matunitlindflem1  22987  cramerlem1  22998  mply1topmatcl  23116  mp2pm2mplem4  23120  ntrin  23372  elnei  23422  neindisj2  23434  ordtopn3  23507  leordtval2  23523  lecldbas  23530  cnrest2  23597  cmpsublem  23710  ptrescn  23951  xkococn  23972  kqfeq  24036  snfbas  24178  neifil  24192  fclsrest  24336  utopsnnei  24561  neipcfilu  24607  psmetsym  24622  psmetge0  24624  xmetge0  24656  xmetsym  24659  metustto  24865  metustbl  24878  restmetu  24882  nm2dif  24937  nmtri  24938  cnmet  25083  cnmpopc  25242  iihalf1  25245  iihalf2  25247  iocopnst  25254  clmnegsubdi2  25419  clmsub4  25420  clmvsubval2  25424  ncvspi  25470  cphsqrtcl3  25501  cph2ass  25527  cphipval2  25555  cphipval  25557  caublcls  25623  bcthlem3  25640  bcthlem4  25641  srabn  25674  cssbn  25689  cmslsschl  25691  rrxmet  25722  rrxdsfi  25725  iblconst  26131  dvdsq1p  26474  coeid3  26552  aannenlem2  26649  pserdvlem2  26748  tanord1  26858  cxpef  26986  recxpcl  26996  logbchbase  27092  relogbcl  27094  relogbzcl  27095  logbleb  27104  logblt  27105  relogbcxpb  27108  lawcos  27137  pythag  27138  isosctrlem1  27139  isosctrlem2  27140  lgsmodeq  27662  lgsmulsqcoprm  27663  gausslemma2dlem1a  27685  2lgsoddprmlem2  27729  ltsres  28012  lestr  28112  cofcutr  28303  lrrecpo  28320  ltadds2im  28365  leadds2im  28367  leadds1  28368  leadds2  28369  ltadds1  28371  addscan2  28372  addscan1  28373  ltsubs1  28455  divmulsw  28572  oldfib  28756  zsoring  28788  bdayfinbndlem1  28846  ax5seglem1  29499  axcontlem2  29536  axcontlem8  29542  upgrpredgv  29710  numedglnl  29715  issubgr2  29846  uhgrissubgr  29849  egrsubgr  29851  nbusgrfi  29948  nb3grprlem2  29955  cplgr3v  30009  cusgrsizeindslem  30025  finsumvtxdg2size  30124  rusgrpropadjvtx  30159  upgrwlkvtxedg  30218  swrdwlk  30261  usgr2trlncl  30339  uspgrn2crct  30390  crctcshwlkn0lem4  30395  crctcshwlkn0lem5  30396  wwlksnextproplem3  30493  umgr2adedgwlklem  30526  rusgr0edg  30558  clwwlk1loop  30572  clwwlkccatlem  30573  clwlkclwwlklem2a4  30581  clwlkclwwlklem2a  30582  clwwisshclwwslemlem  30597  erclwwlktr  30606  clwwlkel  30630  erclwwlkntr  30655  clwwlknonex2lem2  30692  uhgr3cyclex  30776  umgr3cyclex  30777  eucrctshift  30837  frgr3v  30869  3cyclfrgrrn  30880  frgrwopreglem5a  30905  frgr2wsp1  30924  extwwlkfab  30946  clwwlknonclwlknonf1o  30956  numclwwlk3lem1  30976  numclwwlk5  30982  numclwwlk6  30984  isgrpo  31092  grpoinvid1  31123  grpoinvid2  31124  grpoinvop  31128  grpodivinv  31131  grpoinvdiv  31132  grpodivf  31133  grponpcan  31138  ablonncan  31151  nvmval  31237  nvmval2  31238  nvmfval  31239  nvmul0or  31245  nvpncan2  31248  nvaddsub4  31252  nvmeq0  31253  nvdif  31261  nvpi  31262  nvmtri  31266  nvabs  31267  imsmetlem  31285  ipval2lem3  31300  ipval2  31302  4ipval2  31303  ipval3  31304  nmooge0  31362  blometi  31398  hvaddsub12  31633  hvsubdistr1  31644  hvsubdistr2  31645  hvaddcan2  31666  hvmulcan  31667  hvmulcan2  31668  hvsubcan  31669  hvsubcan2  31670  his7  31685  his2sub  31687  his2sub2  31688  norm3dif2  31746  shsubcl  31815  hhssnv  31859  shlej2  31956  fh2  32214  cm2j  32215  pjoi0  32312  hodcl  32342  hosubdi  32403  unopf1o  32511  unopadj  32514  adj2  32529  braadd  32540  bramul  32541  lnopaddmuli  32568  lnopsubmuli  32570  homco2  32572  lnfnaddmuli  32640  adjlnop  32681  leopmul  32729  leoptr  32732  pjimai  32771  atcv1  32975  atexch  32976  atcvatlem  32980  fcoinvbr  33192  preiman0  33296  divnumden2  33400  xdivmul  33484  cshf1o  33516  resvsca  33886  idlsrgcmnd  34040  hasheuni  34710  cndprobin  35059  bayesth  35064  signstfvp  35193  breprexplemc  35254  trssfir1om  35726  fineqvac  35767  fineqvnttrclselem1  35772  fineqvnttrclselem3  35774  trssfir1omregs  35787  lediv2aALT  36421  fununiq  36513  dfrdg2  36537  clsun  37096  neiin  37100  rdgeqoa  38273  poimirlem32  38550  ftc1anclem4  38594  areacirc  38611  filbcmb  38654  ismtybnd  38721  grpoeqdivid  38795  ghomco  38805  rngonegrmul  38858  zerdivemp1x  38861  rngohomco  38888  rngoisoco  38896  riscer  38902  intidl  38943  isfldidl  38982  eceldmqsxrncnvepres  39348  eceldmqsxrncnvepres2  39349  brredunds  39622  lshpnelb  40021  opnlen0  40225  opcon3b  40233  opcon2b  40234  oplecon3b  40237  opltcon3b  40241  opltcon2b  40243  oldmm1  40254  oldmm4  40257  oldmj1  40258  oldmj4  40261  cvrval2  40311  cvrcon3b  40314  leatb  40329  atcmp  40348  atcvreq0  40351  atlatle  40357  athgt  40493  3dim2  40505  islln2a  40554  lplnnleat  40579  lvolnleat  40620  4atlem10  40643  4atlem11  40646  4atlem12  40649  dalem21  40731  dalem22  40732  dalem23  40733  dalem29  40738  dalem30  40739  dalem31N  40740  dalem32  40741  dalem33  40742  dalem34  40743  dalem35  40744  dalem36  40745  dalem37  40746  dalem40  40749  dalem46  40755  dalem47  40756  dalem51  40760  dalem52  40761  dalem58  40767  dalem59  40768  pmaple  40798  paddclN  40879  pmapjoin  40889  pmapjat1  40890  elpcliN  40930  pclssN  40931  pclun2N  40936  2polcon4bN  40955  paddunN  40964  poldmj1N  40965  pmapj2N  40966  pmapocjN  40967  psubclinN  40985  paddatclN  40986  poml4N  40990  lautco  41134  ldilco  41153  ltrneq2  41185  trljat1  41203  cdlemc1  41228  cdleme10  41291  ltrnco  41756  trlcocnv  41757  trljco  41777  trljco2  41778  cdlemi1  41855  tendocnv  42058  diaord  42084  dibord  42196  dihord3  42294  dihord4  42295  dihmeetlem2N  42336  dihmeetlem4preN  42343  dochdmj1  42427  hdmap10lem  42876  lcmineqlem1  43059  sticksstones2  43177  readdsub  43415  reltsub1  43417  renpncan3  43422  reppncan  43424  resubdi  43427  readdcan2  43444  mzprename  43739  dvdsrabdioph  43796  pell14qrdivcl  43851  monotoddzz  43929  jm2.19lem2  43976  jm2.19  43979  relexpaddss  44703  k0004lem3  45134  dvconstbi  45303  chordthmALT  45900  isosctrlem1ALT  45901  ssinc  46071  ssdec  46072  wessf1ornlem  46169  disjf1o  46175  ssnnf1octb  46178  projf1o  46180  mapssbi  46195  iunmapsn  46199  upbdrech  46290  iuneqfzuzlem  46315  suplesup  46320  rexabslelem  46397  climxrrelem  46728  limsupresxr  46745  liminfresxr  46746  liminfvalxr  46762  xlimliminflimsup  46841  cncfshift  46853  cncfperiod  46858  cncfuni  46865  icccncfext  46866  dvmptfprodlem  46923  dvnprodlem1  46925  itgspltprt  46958  ismbl3  46965  stoweidlem3  46982  stoweidlem10  46989  stoweidlem19  46998  stoweidlem31  47010  stoweidlem34  47013  stoweidlem44  47023  fourierdlem41  47127  fourierdlem42  47128  fourierdlem51  47136  fourierdlem68  47153  fourierdlem89  47174  fourierdlem91  47176  fourierdlem92  47177  fourierdlem94  47179  etransclem24  47237  etransclem34  47247  qndenserrnbllem  47273  salincl  47303  saldifcl2  47307  subsalsal  47338  sge0pr  47373  sge0pnffigt  47375  sge0reuz  47426  nnfoctbdjlem  47434  nnfoctbdj  47435  meadjiunlem  47444  caratheodorylem2  47506  hoidmv1le  47573  hoidmvlelem3  47576  hspmbllem2  47606  opnvonmbllem2  47612  smfaddlem1  47742  sigaraf  47832  sigarmf  47833  nltle2tri  48352  subsubelfzo0  48366  nnmul2  48369  submodaddmod  48386  zplusmodne  48388  addmodne  48389  minusmod5ne  48394  submodneaddmod  48396  modmkpkne  48406  modmknepk  48407  iccpartiltu  48473  icceuelpart  48487  poprelb  48575  reuopreuprim  48577  nprmmul2  48579  proththd  48668  mogoldbblem  48787  fppr2odd  48798  fpprel2  48808  bgoldbtbndlem2  48873  clnbusgrfi  48910  grimuhgr  48954  uhgrimisgrgric  48998  clnbgrgrim  49001  grtrif1o  49009  grlimgrtri  49070  gpgusgralem  49123  gpgedgvtx0  49128  gpgedg2ov  49133  gpgedg2iv  49134  gpg5nbgrvtx03starlem2  49136  nn0sumltlt  49431  invginvrid  49448  ply1sclrmsm  49465  linccl  49495  lincvalpr  49499  lincresunit3lem1  49560  lincresunit3  49562  fdivmpt  49621  nnolog2flm1  49671  dignnld  49684  digexp  49688  dignn0flhalflem1  49696  itcovalsucov  49749  reorelicc  49791  eenglngeehlnmlem1  49818  line2  49833  line2xlem  49834  itsclc0lem1  49837  itsclc0xyqsolr  49850  i0oii  49997  io1ii  49998  indthinc  50539  indthincALT  50540  reccot  50820  rectan  50821