Theorem 3adant2 1132

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  3ad2ant1  1134  3simpb  1150  3imp3i2an  1347  eupickb  2636  eqeu  3666  onunel  6432  iotan0  6490  funopg  6534  dff1o2  6787  fvelimad  6909  unima  6917  fnimapr  6925  fvmptt  6970  fnreseql  7002  xpprsng  7095  f1elima  7219  f1ounsn  7228  f13dfv  7230  f1ocnvfvb  7235  f1cdmsn  7238  f1ofvswap  7262  oprssov  7537  resf1extb  7886  resf1ext2b  7887  funelss  8001  poxp  8080  poxp2  8095  poxp3  8102  smoiso  8304  oaord  8484  oaword  8486  omcan  8506  omwordri  8509  odi  8516  omeulem1  8519  oeord  8526  oecan  8527  oewordri  8530  oeordsuc  8532  nnaord  8557  nnaordr  8558  nndi  8561  nnaword  8565  nnmwordri  8574  naddel2  8626  naddss1  8627  naddss2  8628  erov  8763  ecopovtrn  8769  mapsnd  8836  f1dom3g  8916  xpdom3  9015  mapxpen  9083  dif1en  9098  findcard  9100  f1domfi2  9118  entrfir  9127  domtrfil  9128  domtrfir  9130  sbthfilem  9134  sdomdomtrfi  9137  php3  9145  findcard3  9195  indexfi  9272  suppr  9387  infpr  9420  r111  9699  tcrank  9808  acndom  9973  infdif2  10131  infxpdom  10132  cfeq0  10178  cfsuc  10179  cfflb  10181  cflim2  10185  cfsmolem  10192  axcc3  10360  domtriomlem  10364  axdc3lem2  10373  axdc3lem4  10375  axdc4lem  10377  axcclem  10379  pwcfsdom  10506  tsktrss  10684  tsksuc  10685  tskuni  10706  adderpqlem  10877  mulerpqlem  10878  mulcanenq  10883  distrnq  10884  ltsonq  10892  ltanq  10894  ltmnq  10895  distrlem1pr  10948  distrlem5pr  10950  ltsopr  10955  ltsosr  11017  ltasr  11023  adddir  11135  axlttrn  11217  letr  11239  nnncan1  11429  npncan3  11431  pnpcan2  11433  subdi  11582  subdir  11583  mulcan1g  11802  mulcan2g  11803  divmul  11811  div23  11827  div13  11829  muldivdir  11846  divsubdir  11847  subdivcomb1  11848  divcan7  11862  ltmul2  12004  lemul1  12005  lemul2  12006  lemul2a  12008  lediv1  12019  ltmuldiv2  12028  lemuldiv  12034  lemuldiv2  12035  ltdiv2  12040  lediv2  12044  infrelb  12139  nndivtr  12204  bndndx  12412  nn0n0n1ge2  12481  fnn0ind  12603  addlelt  13033  xrletr  13084  qsqueeze  13128  xleadd2a  13181  xleadd1  13182  xltadd2  13184  xltmul2  13220  supxrbnd  13255  iooneg  13399  iccneg  13400  icoshft  13401  icoshftf1o  13402  zltaddlt1le  13433  fzen  13469  uzsubsubfz  13474  ssfzunsnext  13497  fzrevral2  13541  fzshftral  13543  fz0fzdiffz0  13565  elfzmlbp  13567  elfzo  13589  nelfzo  13592  fzoaddel2  13648  fzosubel2  13653  ssfzo12bi  13689  fzonfzoufzol  13699  subfzo0  13720  flltdivnn0lt  13765  modmulnn  13821  modcyc  13838  modaddabs  13843  modaddmod  13844  modmuladd  13848  modadd2mod  13856  modsubmod  13864  modsubmodmod  13865  modaddmodup  13869  modmulmod  13871  modsubdir  13875  modfzo0difsn  13878  modsumfzodifsn  13879  uzindi  13917  axdc4uzlem  13918  expneg2  14005  expdiv  14048  expubnd  14113  mulbinom2  14158  bernneq2  14165  expnngt1  14176  hashinfxadd  14320  hashunsngx  14328  hashunsnggt  14329  hashfundm  14377  hashf1dmcdm  14379  hashdifsnp1  14441  ccatval3  14514  ccatfv0  14519  ccatval1lsw  14520  ccats1val2  14563  ccatw2s1p1  14572  swrdnd  14590  pfxsuffeqwrdeq  14633  pfxsuff1eqwrdeq  14634  swrdswrd  14640  pfxpfx  14643  wrd2ind  14658  swrdccatin1  14660  pfxccatin12lem1  14663  swrdccatin2  14664  pfxccatin12lem3  14667  swrdccat  14670  pfxccatpfx1  14671  pfxccatpfx2  14672  swrdccat3blem  14674  repswswrd  14719  repswpfx  14720  repswccat  14721  cshwidxmod  14738  2cshw  14748  3cshw  14753  scshwfzeqfzo  14761  cshwcsh2id  14763  cshimadifsn  14764  cshimadifsn0  14765  ccatco  14770  cshco  14771  swrdco  14772  pfxco  14773  lswco  14774  swrds2  14875  2swrd2eqwrdeq  14888  shftuz  15004  abs3dif  15267  fsumdifsnconst  15726  modfsummods  15728  sin02gt0  16129  dvdsval2  16194  dvdscmul  16221  dvdsmulc  16222  dvdscmulr  16223  dvdsmulcr  16224  divalglem8  16339  ndvdssub  16348  dvdsexpim  16494  rpmulgcd  16496  expgcd  16502  zexpgcd  16504  coprmprod  16600  cncongr1  16606  cncongr2  16607  isprm3  16622  modprm0  16745  coprimeprodsq  16748  pythagtriplem12  16766  pythagtriplem14  16768  pcprendvds  16780  pcmul  16791  pcdiv  16792  pcqcl  16796  pcqdiv  16797  pcdvdsb  16809  vdwnnlem1  16935  hashbcss  16944  cshwshashlem1  17035  fvsetsid  17107  setsstruct2  17113  setsstruct  17115  mrcss  17551  mrcsscl  17555  mrcun  17557  cofulid  17826  catcisolem  18046  funcsetcestrclem9  18098  latleeqj1  18386  lubun  18450  clatleglb  18453  pslem  18507  dirtr  18537  mgmb1mgm1  18592  pwspjmhm  18767  grpinvid1  18933  grpinvid2  18934  grpasscan1  18943  grpasscan2  18944  grpinvadd  18960  grpsubf  18961  grpsubrcan  18963  grpinvsub  18964  grpsubeq0  18968  grpsubadd0sub  18969  grppncan  18973  grpnpcan  18974  mulgnn0p1  19027  mulgaddcomlem  19039  mulginvcom  19041  mulginvinv  19042  subgsubcl  19079  subgsub  19080  eqglact  19120  qussub  19132  ghmsub  19165  psgnunilem4  19438  oddvds2  19507  odsubdvds  19512  gexnnod  19529  slwn0  19556  dvrcl  20352  unitdvcl  20353  dvrcan1  20357  dvrcan3  20358  dvreq1  20359  rngisom1  20414  rngisomring  20415  subrgdv  20534  abvsubtri  20772  idsrngd  20801  lmodvsubval2  20880  lsmcl  21047  lsmsp2  21051  lspsntrim  21062  rngqiprngimfolem  21257  lidldvgen  21301  cncrng  21355  chrcong  21494  dvdschrmulg  21495  zndvds  21516  zntoslem  21523  ocvsscon  21642  obselocv  21695  frlmphl  21748  ascldimul  21856  mpfsubrg  22078  ply1tmcl  22226  eqcoe1ply1eq  22255  gsummoncoe1  22264  lply1binomsc  22267  mamudm  22351  mamufacex  22352  scmatf1  22487  scmatf1o  22488  scmatrngiso  22492  submabas  22534  mdetdiaglem  22554  mdetralt2  22565  mdetero  22566  mdetunilem2  22569  mdetunilem6  22573  m2detleiblem7  22583  maducoeval2  22596  gsummatr01lem3  22613  gsummatr01  22615  smadiadetglem2  22628  cramerlem1  22643  mply1topmatcl  22761  mp2pm2mplem4  22765  ntrin  23017  elnei  23067  neindisj2  23079  ordtopn3  23152  leordtval2  23168  lecldbas  23175  cnrest2  23242  cmpsublem  23355  ptrescn  23595  xkococn  23616  kqfeq  23680  snfbas  23822  neifil  23836  fclsrest  23980  utopsnnei  24205  neipcfilu  24251  psmetsym  24266  psmetge0  24268  xmetge0  24300  xmetsym  24303  metustto  24509  metustbl  24522  restmetu  24526  nm2dif  24581  nmtri  24582  cnmet  24727  cnmpopc  24890  iihalf1  24893  iihalf2  24896  iocopnst  24905  clmnegsubdi2  25073  clmsub4  25074  clmvsubval2  25078  ncvspi  25124  cphsqrtcl3  25155  cph2ass  25181  cphipval2  25209  cphipval  25211  caublcls  25277  bcthlem3  25294  bcthlem4  25295  srabn  25328  cssbn  25343  cmslsschl  25345  rrxmet  25376  rrxdsfi  25379  iblconst  25787  dvdsq1p  26136  coeid3  26213  aannenlem2  26305  pserdvlem2  26406  tanord1  26514  cxpef  26642  recxpcl  26652  logbchbase  26749  relogbcl  26751  relogbzcl  26752  logbleb  26761  logblt  26762  relogbcxpb  26765  lawcos  26794  pythag  26795  isosctrlem1  26796  isosctrlem2  26797  lgsmodeq  27321  lgsmulsqcoprm  27322  gausslemma2dlem1a  27344  2lgsoddprmlem2  27388  ltsres  27642  lestr  27742  cofcutr  27932  lrrecpo  27949  ltadds2im  27994  leadds2im  27996  leadds1  27997  leadds2  27998  ltadds1  28000  addscan2  28001  addscan1  28002  ltsubs1  28084  divmulsw  28201  oldfib  28385  zsoring  28417  bdayfinbndlem1  28475  ax5seglem1  29013  axcontlem2  29050  axcontlem8  29056  upgrpredgv  29224  numedglnl  29229  issubgr2  29357  uhgrissubgr  29360  egrsubgr  29362  nbusgrfi  29459  nb3grprlem2  29466  cplgr3v  29520  cusgrsizeindslem  29537  finsumvtxdg2size  29636  rusgrpropadjvtx  29671  upgrwlkvtxedg  29730  usgr2trlncl  29845  uspgrn2crct  29893  crctcshwlkn0lem4  29898  crctcshwlkn0lem5  29899  wwlksnextproplem3  29996  umgr2adedgwlklem  30029  rusgr0edg  30061  clwwlk1loop  30075  clwwlkccatlem  30076  clwlkclwwlklem2a4  30084  clwlkclwwlklem2a  30085  clwwisshclwwslemlem  30100  erclwwlktr  30109  clwwlkel  30133  erclwwlkntr  30158  clwwlknonex2lem2  30195  uhgr3cyclex  30269  umgr3cyclex  30270  eucrctshift  30330  frgr3v  30362  3cyclfrgrrn  30373  frgrwopreglem5a  30398  frgr2wsp1  30417  extwwlkfab  30439  clwwlknonclwlknonf1o  30449  numclwwlk3lem1  30469  numclwwlk5  30475  numclwwlk6  30477  isgrpo  30584  grpoinvid1  30615  grpoinvid2  30616  grpoinvop  30620  grpodivinv  30623  grpoinvdiv  30624  grpodivf  30625  grponpcan  30630  ablonncan  30643  nvmval  30729  nvmval2  30730  nvmfval  30731  nvmul0or  30737  nvpncan2  30740  nvaddsub4  30744  nvmeq0  30745  nvdif  30753  nvpi  30754  nvmtri  30758  nvabs  30759  imsmetlem  30777  ipval2lem3  30792  ipval2  30794  4ipval2  30795  ipval3  30796  nmooge0  30854  blometi  30890  hvaddsub12  31125  hvsubdistr1  31136  hvsubdistr2  31137  hvaddcan2  31158  hvmulcan  31159  hvmulcan2  31160  hvsubcan  31161  hvsubcan2  31162  his7  31177  his2sub  31179  his2sub2  31180  norm3dif2  31238  shsubcl  31307  hhssnv  31351  shlej2  31448  fh2  31706  cm2j  31707  pjoi0  31804  hodcl  31834  hosubdi  31895  unopf1o  32003  unopadj  32006  adj2  32021  braadd  32032  bramul  32033  lnopaddmuli  32060  lnopsubmuli  32062  homco2  32064  lnfnaddmuli  32132  adjlnop  32173  leopmul  32221  leoptr  32224  pjimai  32263  atcv1  32467  atexch  32468  atcvatlem  32472  fcoinvbr  32691  preiman0  32799  divnumden2  32906  sgn3da  32925  xdivmul  33016  cshf1o  33054  resvsca  33424  idlsrgcmnd  33607  hasheuni  34262  difelsiga  34310  cndprobin  34611  bayesth  34616  signstfvp  34748  breprexplemc  34809  trssfir1om  35286  fineqvac  35291  fineqvnttrclselem1  35296  fineqvnttrclselem3  35298  trssfir1omregs  35311  swrdrevpfx  35330  swrdwlk  35340  lediv2aALT  35890  fununiq  35982  dfrdg2  36006  clsun  36541  neiin  36545  rdgeqoa  37622  curfv  37848  matunitlindflem1  37864  poimirlem32  37900  ftc1anclem4  37944  areacirc  37961  filbcmb  37988  ismtybnd  38055  grpoeqdivid  38129  ghomco  38139  rngonegrmul  38192  zerdivemp1x  38195  rngohomco  38222  rngoisoco  38230  riscer  38236  intidl  38277  isfldidl  38316  eceldmqsxrncnvepres  38684  eceldmqsxrncnvepres2  38685  brredunds  38958  lshpnelb  39357  opnlen0  39561  opcon3b  39569  opcon2b  39570  oplecon3b  39573  opltcon3b  39577  opltcon2b  39579  oldmm1  39590  oldmm4  39593  oldmj1  39594  oldmj4  39597  cvrval2  39647  cvrcon3b  39650  leatb  39665  atcmp  39684  atcvreq0  39687  atlatle  39693  athgt  39829  3dim2  39841  islln2a  39890  lplnnleat  39915  lvolnleat  39956  4atlem10  39979  4atlem11  39982  4atlem12  39985  dalem21  40067  dalem22  40068  dalem23  40069  dalem29  40074  dalem30  40075  dalem31N  40076  dalem32  40077  dalem33  40078  dalem34  40079  dalem35  40080  dalem36  40081  dalem37  40082  dalem40  40085  dalem46  40091  dalem47  40092  dalem51  40096  dalem52  40097  dalem58  40103  dalem59  40104  pmaple  40134  paddclN  40215  pmapjoin  40225  pmapjat1  40226  elpcliN  40266  pclssN  40267  pclun2N  40272  2polcon4bN  40291  paddunN  40300  poldmj1N  40301  pmapj2N  40302  pmapocjN  40303  psubclinN  40321  paddatclN  40322  poml4N  40326  lautco  40470  ldilco  40489  ltrneq2  40521  trljat1  40539  cdlemc1  40564  cdleme10  40627  ltrnco  41092  trlcocnv  41093  trljco  41113  trljco2  41114  cdlemi1  41191  tendocnv  41394  diaord  41420  dibord  41532  dihord3  41630  dihord4  41631  dihmeetlem2N  41672  dihmeetlem4preN  41679  dochdmj1  41763  hdmap10lem  42212  lcmineqlem1  42396  sticksstones2  42514  readdsub  42751  reltsub1  42753  renpncan3  42758  reppncan  42760  resubdi  42763  readdcan2  42780  mzprename  43103  dvdsrabdioph  43164  pell14qrdivcl  43219  monotoddzz  43297  jm2.19lem2  43344  jm2.19  43347  relexpaddss  44071  k0004lem3  44502  dvconstbi  44687  chordthmALT  45285  isosctrlem1ALT  45286  ssinc  45443  ssdec  45444  wessf1ornlem  45541  disjf1o  45547  ssnnf1octb  45550  projf1o  45552  mapssbi  45568  iunmapsn  45572  upbdrech  45664  iuneqfzuzlem  45690  suplesup  45695  rexabslelem  45773  climxrrelem  46104  limsupresxr  46121  liminfresxr  46122  liminfvalxr  46138  xlimliminflimsup  46217  cncfshift  46229  cncfperiod  46234  cncfuni  46241  icccncfext  46242  dvmptfprodlem  46299  dvnprodlem1  46301  itgspltprt  46334  ismbl3  46341  stoweidlem3  46358  stoweidlem10  46365  stoweidlem19  46374  stoweidlem31  46386  stoweidlem34  46389  stoweidlem44  46399  fourierdlem41  46503  fourierdlem42  46504  fourierdlem51  46512  fourierdlem68  46529  fourierdlem89  46550  fourierdlem91  46552  fourierdlem92  46553  fourierdlem94  46555  etransclem24  46613  etransclem34  46623  qndenserrnbllem  46649  salincl  46679  saldifcl2  46683  subsalsal  46714  sge0pr  46749  sge0pnffigt  46751  sge0reuz  46802  nnfoctbdjlem  46810  nnfoctbdj  46811  meadjiunlem  46820  caratheodorylem2  46882  hoidmv1le  46949  hoidmvlelem3  46952  hspmbllem2  46982  opnvonmbllem2  46988  sssmf  47093  smfaddlem1  47118  sigaraf  47208  sigarmf  47209  nltle2tri  47670  subsubelfzo0  47683  submodaddmod  47698  zplusmodne  47700  addmodne  47701  minusmod5ne  47706  submodneaddmod  47708  modmkpkne  47718  modmknepk  47719  iccpartiltu  47779  icceuelpart  47793  poprelb  47881  reuopreuprim  47883  proththd  47971  mogoldbblem  48077  fppr2odd  48088  fpprel2  48098  bgoldbtbndlem2  48163  clnbusgrfi  48200  grimuhgr  48244  uhgrimisgrgric  48288  clnbgrgrim  48291  grtrif1o  48299  grlimgrtri  48360  gpgusgralem  48413  gpgedgvtx0  48418  gpgedg2ov  48423  gpgedg2iv  48424  gpg5nbgrvtx03starlem2  48426  nn0sumltlt  48707  invginvrid  48724  ply1sclrmsm  48741  linccl  48771  lincvalpr  48775  lincresunit3lem1  48836  lincresunit3  48838  fdivmpt  48897  nnolog2flm1  48947  dignnld  48960  digexp  48964  dignn0flhalflem1  48972  itcovalsucov  49025  reorelicc  49067  eenglngeehlnmlem1  49094  line2  49109  line2xlem  49110  itsclc0lem1  49113  itsclc0xyqsolr  49126  i0oii  49276  io1ii  49277  indthinc  49818  indthincALT  49819  setrec2fun  50048  reccot  50114  rectan  50115