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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 398  df-3an 1090

This theorem is referenced by:  3ad2ant1  1134  3simpb  1150  3imp3i2an  1346  eupickb  2632  vtoclegftOLD  3575  eqeu  3703  onunel  6470  iotan0  6534  funopg  6583  fncoOLD  6669  dff1o2  6839  fvelimad  6960  unima  6967  fnimapr  6976  fvmptt  7019  fnreseql  7050  xpprsng  7138  f1elima  7262  f13dfv  7272  f1ocnvfvb  7277  f1cdmsn  7280  f1ofvswap  7304  oprssov  7576  funelss  8033  poxp  8114  poxp2  8129  poxp3  8136  wfrlem4OLD  8312  smoiso  8362  oaord  8547  oaword  8549  omcan  8569  omwordri  8572  odi  8579  omeulem1  8582  oeord  8588  oecan  8589  oewordri  8592  oeordsuc  8594  nnaord  8619  nnaordr  8620  nndi  8623  nnaword  8627  nnmwordri  8636  naddel2  8687  naddss1  8688  naddss2  8689  erov  8808  ecopovtrn  8814  mapsnd  8880  f1dom3g  8963  xpdom3  9070  mapxpen  9143  dif1en  9160  dif1enOLD  9162  findcard  9163  f1domfi2  9185  entrfir  9194  domtrfil  9195  domtrfir  9197  sbthfilem  9201  sdomdomtrfi  9204  php3  9212  findcard3  9285  indexfi  9360  suppr  9466  infpr  9498  r111  9770  tcrank  9879  acndom  10046  infdif2  10205  infxpdom  10206  cfeq0  10251  cfsuc  10252  cfflb  10254  cflim2  10258  cfsmolem  10265  axcc3  10433  domtriomlem  10437  axdc3lem2  10446  axdc3lem4  10448  axdc4lem  10450  axcclem  10452  pwcfsdom  10578  tsktrss  10756  tsksuc  10757  tskuni  10778  adderpqlem  10949  mulerpqlem  10950  mulcanenq  10955  distrnq  10956  ltsonq  10964  ltanq  10966  ltmnq  10967  distrlem1pr  11020  distrlem5pr  11022  ltsopr  11027  ltsosr  11089  ltasr  11095  adddir  11205  axlttrn  11286  letr  11308  nnncan1  11496  npncan3  11498  pnpcan2  11500  subdi  11647  subdir  11648  mulcan1g  11867  mulcan2g  11868  divmul  11875  div23  11891  div13  11893  muldivdir  11907  divsubdir  11908  subdivcomb1  11909  divcan7  11923  ltmul2  12065  lemul1  12066  lemul2  12067  lemul2a  12069  lediv1  12079  ltmuldiv2  12088  lemuldiv  12094  lemuldiv2  12095  ltdiv2  12100  lediv2  12104  infrelb  12199  nndivtr  12259  bndndx  12471  nn0n0n1ge2  12539  fnn0ind  12661  addlelt  13088  xrletr  13137  qsqueeze  13180  xleadd2a  13233  xleadd1  13234  xltadd2  13236  xltmul2  13272  supxrbnd  13307  iooneg  13448  iccneg  13449  icoshft  13450  icoshftf1o  13451  zltaddlt1le  13482  fzen  13518  uzsubsubfz  13523  ssfzunsnext  13546  fzrevral2  13587  fzshftral  13589  fz0fzdiffz0  13610  elfzmlbp  13612  elfzo  13634  nelfzo  13637  fzoaddel2  13688  fzosubel2  13692  ssfzo12bi  13727  fzonfzoufzol  13735  subfzo0  13754  flltdivnn0lt  13798  modmulnn  13854  modcyc  13871  modaddabs  13874  modaddmod  13875  modmuladd  13878  modadd2mod  13886  modsubmod  13894  modsubmodmod  13895  modaddmodup  13899  modmulmod  13901  modsubdir  13905  modfzo0difsn  13908  modsumfzodifsn  13909  uzindi  13947  axdc4uzlem  13948  expneg2  14036  expdiv  14079  expubnd  14142  mulbinom2  14186  bernneq2  14193  expnngt1  14204  hashinfxadd  14345  hashunsngx  14353  hashunsnggt  14354  hashfundm  14402  hashdifsnp1  14457  ccatval3  14529  ccatfv0  14533  ccatval1lsw  14534  ccats1val2  14577  ccatw2s1p1  14586  swrdnd  14604  pfxsuffeqwrdeq  14648  pfxsuff1eqwrdeq  14649  swrdswrd  14655  pfxpfx  14658  wrd2ind  14673  swrdccatin1  14675  pfxccatin12lem1  14678  swrdccatin2  14679  pfxccatin12lem3  14682  swrdccat  14685  pfxccatpfx1  14686  pfxccatpfx2  14687  swrdccat3blem  14689  repswswrd  14734  repswpfx  14735  repswccat  14736  cshwidxmod  14753  2cshw  14763  3cshw  14768  scshwfzeqfzo  14777  cshwcsh2id  14779  cshimadifsn  14780  cshimadifsn0  14781  ccatco  14786  cshco  14787  swrdco  14788  pfxco  14789  lswco  14790  swrds2  14891  2swrd2eqwrdeq  14904  shftuz  15016  abs3dif  15278  fsumdifsnconst  15737  modfsummods  15739  sin02gt0  16135  dvdsval2  16200  dvdscmul  16226  dvdsmulc  16227  dvdscmulr  16228  dvdsmulcr  16229  divalglem8  16343  ndvdssub  16352  rpmulgcd  16498  coprmprod  16598  cncongr1  16604  cncongr2  16605  isprm3  16620  modprm0  16738  coprimeprodsq  16741  pythagtriplem12  16759  pythagtriplem14  16761  pcprendvds  16773  pcmul  16784  pcdiv  16785  pcqcl  16789  pcqdiv  16790  pcdvdsb  16802  vdwnnlem1  16928  hashbcss  16937  cshwshashlem1  17029  fvsetsid  17101  setsstruct2  17107  setsstruct  17109  mrcss  17560  mrcsscl  17564  mrcun  17566  cofulid  17840  catcisolem  18060  funcsetcestrclem9  18115  latleeqj1  18404  lubun  18468  clatleglb  18471  pslem  18525  dirtr  18555  mgmb1mgm1  18574  pwspjmhm  18711  grpinvid1  18876  grpinvid2  18877  grpasscan1  18886  grpasscan2  18887  grpinvadd  18901  grpsubf  18902  grpsubrcan  18904  grpinvsub  18905  grpsubeq0  18909  grpsubadd0sub  18910  grppncan  18914  grpnpcan  18915  mulgnn0p1  18965  mulgaddcomlem  18977  mulginvcom  18979  mulginvinv  18980  subgsubcl  19017  subgsub  19018  eqglact  19059  qussub  19070  ghmsub  19100  psgnunilem4  19365  oddvds2  19434  odsubdvds  19439  gexnnod  19456  slwn0  19483  dvrcl  20218  unitdvcl  20219  dvrcan1  20223  dvrcan3  20224  dvreq1  20225  subrgdv  20336  abvsubtri  20443  idsrngd  20470  lmodvsubval2  20527  lsmcl  20694  lsmsp2  20698  lspsntrim  20709  lidldvgen  20893  chrcong  21081  zndvds  21105  zntoslem  21112  ocvsscon  21228  obselocv  21283  frlmphl  21336  ascldimul  21442  mpfsubrg  21666  ply1tmcl  21794  eqcoe1ply1eq  21821  gsummoncoe1  21828  lply1binomsc  21831  mamudm  21890  mamufacex  21891  scmatf1  22033  scmatf1o  22034  scmatrngiso  22038  submabas  22080  mdetdiaglem  22100  mdetralt2  22111  mdetero  22112  mdetunilem2  22115  mdetunilem6  22119  m2detleiblem7  22129  maducoeval2  22142  gsummatr01lem3  22159  gsummatr01  22161  smadiadetglem2  22174  cramerlem1  22189  mply1topmatcl  22307  mp2pm2mplem4  22311  ntrin  22565  elnei  22615  neindisj2  22627  ordtopn3  22700  leordtval2  22716  lecldbas  22723  cnrest2  22790  cmpsublem  22903  ptrescn  23143  xkococn  23164  kqfeq  23228  snfbas  23370  neifil  23384  fclsrest  23528  utopsnnei  23754  neipcfilu  23801  psmetsym  23816  psmetge0  23818  xmetge0  23850  xmetsym  23853  metustto  24062  metustbl  24075  restmetu  24079  nm2dif  24134  nmtri  24135  cnmet  24288  cnmpopc  24444  iihalf1  24447  iihalf2  24449  iocopnst  24456  clmnegsubdi2  24621  clmsub4  24622  clmvsubval2  24626  ncvspi  24673  cphsqrtcl3  24704  cph2ass  24730  cphipval2  24758  cphipval  24760  caublcls  24826  bcthlem3  24843  bcthlem4  24844  srabn  24877  cssbn  24892  cmslsschl  24894  rrxmet  24925  rrxdsfi  24928  iblconst  25335  tdeglem3OLD  25576  dvdsq1p  25678  coeid3  25754  aannenlem2  25842  pserdvlem2  25940  tanord1  26046  cxpef  26173  recxpcl  26183  logbchbase  26276  relogbcl  26278  relogbzcl  26279  logbleb  26288  logblt  26289  relogbcxpb  26292  lawcos  26321  pythag  26322  isosctrlem1  26323  isosctrlem2  26324  lgsmodeq  26845  lgsmulsqcoprm  26846  gausslemma2dlem1a  26868  2lgsoddprmlem2  26912  sltres  27165  sletr  27261  cofcutr  27413  lrrecpo  27427  sltadd2im  27472  sleadd2im  27474  sleadd1  27475  sleadd2  27476  sltadd1  27478  addscan2  27479  addscan1  27480  sltsub1  27546  divsmulw  27643  ax5seglem1  28217  axcontlem2  28254  axcontlem8  28260  upgrpredgv  28430  numedglnl  28435  issubgr2  28560  uhgrissubgr  28563  egrsubgr  28565  nbusgrfi  28662  nb3grprlem2  28669  cplgr3v  28723  cusgrsizeindslem  28739  finsumvtxdg2size  28838  rusgrpropadjvtx  28873  upgrwlkvtxedg  28933  usgr2trlncl  29048  uspgrn2crct  29093  crctcshwlkn0lem4  29098  crctcshwlkn0lem5  29099  wwlksnextproplem3  29196  umgr2adedgwlklem  29229  rusgr0edg  29258  clwwlk1loop  29272  clwwlkccatlem  29273  clwlkclwwlklem2a4  29281  clwlkclwwlklem2a  29282  clwwisshclwwslemlem  29297  erclwwlktr  29306  clwwlkel  29330  erclwwlkntr  29355  clwwlknonex2lem2  29392  uhgr3cyclex  29466  umgr3cyclex  29467  eucrctshift  29527  frgr3v  29559  3cyclfrgrrn  29570  frgrwopreglem5a  29595  frgr2wsp1  29614  extwwlkfab  29636  clwwlknonclwlknonf1o  29646  numclwwlk3lem1  29666  numclwwlk5  29672  numclwwlk6  29674  isgrpo  29781  grpoinvid1  29812  grpoinvid2  29813  grpoinvop  29817  grpodivinv  29820  grpoinvdiv  29821  grpodivf  29822  grponpcan  29827  ablonncan  29840  nvmval  29926  nvmval2  29927  nvmfval  29928  nvmul0or  29934  nvpncan2  29937  nvaddsub4  29941  nvmeq0  29942  nvdif  29950  nvpi  29951  nvmtri  29955  nvabs  29956  imsmetlem  29974  ipval2lem3  29989  ipval2  29991  4ipval2  29992  ipval3  29993  nmooge0  30051  blometi  30087  hvaddsub12  30322  hvsubdistr1  30333  hvsubdistr2  30334  hvaddcan2  30355  hvmulcan  30356  hvmulcan2  30357  hvsubcan  30358  hvsubcan2  30359  his7  30374  his2sub  30376  his2sub2  30377  norm3dif2  30435  shsubcl  30504  hhssnv  30548  shlej2  30645  fh2  30903  cm2j  30904  pjoi0  31001  hodcl  31031  hosubdi  31092  unopf1o  31200  unopadj  31203  adj2  31218  braadd  31229  bramul  31230  lnopaddmuli  31257  lnopsubmuli  31259  homco2  31261  lnfnaddmuli  31329  adjlnop  31370  leopmul  31418  leoptr  31421  pjimai  31460  atcv1  31664  atexch  31665  atcvatlem  31669  fcoinvbr  31867  preiman0  31962  divnumden2  32055  xdivmul  32122  cshf1o  32157  dvdschrmulg  32411  resvsca  32475  idlsrgcmnd  32660  hasheuni  33114  difelsiga  33162  cndprobin  33464  bayesth  33469  sgn3da  33571  signstfvp  33613  breprexplemc  33675  fineqvac  34128  hashf1dmcdm  34136  swrdrevpfx  34138  swrdwlk  34148  lediv2aALT  34693  fununiq  34771  dfrdg2  34798  clsun  35261  neiin  35265  rdgeqoa  36299  curfv  36516  matunitlindflem1  36532  poimirlem32  36568  ftc1anclem4  36612  areacirc  36629  filbcmb  36656  ismtybnd  36723  grpoeqdivid  36797  ghomco  36807  rngonegrmul  36860  zerdivemp1x  36863  rngohomco  36890  rngoisoco  36898  riscer  36904  intidl  36945  isfldidl  36984  brredunds  37544  lshpnelb  37902  opnlen0  38106  opcon3b  38114  opcon2b  38115  oplecon3b  38118  opltcon3b  38122  opltcon2b  38124  oldmm1  38135  oldmm4  38138  oldmj1  38139  oldmj4  38142  cvrval2  38192  cvrcon3b  38195  leatb  38210  atcmp  38229  atcvreq0  38232  atlatle  38238  athgt  38375  3dim2  38387  islln2a  38436  lplnnleat  38461  lvolnleat  38502  4atlem10  38525  4atlem11  38528  4atlem12  38531  dalem21  38613  dalem22  38614  dalem23  38615  dalem29  38620  dalem30  38621  dalem31N  38622  dalem32  38623  dalem33  38624  dalem34  38625  dalem35  38626  dalem36  38627  dalem37  38628  dalem40  38631  dalem46  38637  dalem47  38638  dalem51  38642  dalem52  38643  dalem58  38649  dalem59  38650  pmaple  38680  paddclN  38761  pmapjoin  38771  pmapjat1  38772  elpcliN  38812  pclssN  38813  pclun2N  38818  2polcon4bN  38837  paddunN  38846  poldmj1N  38847  pmapj2N  38848  pmapocjN  38849  psubclinN  38867  paddatclN  38868  poml4N  38872  lautco  39016  ldilco  39035  ltrneq2  39067  trljat1  39085  cdlemc1  39110  cdleme10  39173  ltrnco  39638  trlcocnv  39639  trljco  39659  trljco2  39660  cdlemi1  39737  tendocnv  39940  diaord  39966  dibord  40078  dihord3  40176  dihord4  40177  dihmeetlem2N  40218  dihmeetlem4preN  40225  dochdmj1  40309  hdmap10lem  40758  lcmineqlem1  40942  sticksstones2  41011  metakunt29  41061  metakunt30  41062  factwoffsmonot  41071  dvdsexpim  41267  expgcd  41273  zexpgcd  41275  readdsub  41305  reltsub1  41307  renpncan3  41312  reppncan  41314  resubdi  41317  readdcan2  41333  mzprename  41535  dvdsrabdioph  41596  pell14qrdivcl  41651  monotoddzz  41730  jm2.19lem2  41777  jm2.19  41780  relexpaddss  42517  k0004lem3  42948  dvconstbi  43141  chordthmALT  43742  isosctrlem1ALT  43743  ssinc  43824  ssdec  43825  wessf1ornlem  43930  disjf1o  43937  ssnnf1octb  43941  projf1o  43944  mapssbi  43960  iunmapsn  43964  upbdrech  44063  iuneqfzuzlem  44092  suplesup  44097  rexabslelem  44176  climxrrelem  44513  limsupresxr  44530  liminfresxr  44531  liminfvalxr  44547  xlimliminflimsup  44626  cncfshift  44638  cncfperiod  44643  cncfuni  44650  icccncfext  44651  dvmptfprodlem  44708  dvnprodlem1  44710  itgspltprt  44743  ismbl3  44750  stoweidlem3  44767  stoweidlem10  44774  stoweidlem19  44783  stoweidlem31  44795  stoweidlem34  44798  stoweidlem44  44808  fourierdlem41  44912  fourierdlem42  44913  fourierdlem51  44921  fourierdlem68  44938  fourierdlem89  44959  fourierdlem91  44961  fourierdlem92  44962  fourierdlem94  44964  etransclem24  45022  etransclem34  45032  qndenserrnbllem  45058  salincl  45088  saldifcl2  45092  subsalsal  45123  sge0pr  45158  sge0pnffigt  45160  sge0reuz  45211  nnfoctbdjlem  45219  nnfoctbdj  45220  meadjiunlem  45229  caratheodorylem2  45291  hoidmv1le  45358  hoidmvlelem3  45361  hspmbllem2  45391  opnvonmbllem2  45397  sssmf  45502  smfaddlem1  45527  sigaraf  45617  sigarmf  45618  nltle2tri  46069  subsubelfzo0  46082  iccpartiltu  46138  icceuelpart  46152  poprelb  46240  reuopreuprim  46242  proththd  46330  mogoldbblem  46436  fppr2odd  46447  fpprel2  46457  bgoldbtbndlem2  46522  isomgrtr  46555  rngisom1  46766  rngisomring  46767  rngqiprngimfolem  46823  nn0sumltlt  47074  invginvrid  47091  ply1sclrmsm  47112  linccl  47143  lincvalpr  47147  lincresunit3lem1  47208  lincresunit3  47210  fdivmpt  47274  nnolog2flm1  47324  dignnld  47337  digexp  47341  dignn0flhalflem1  47349  itcovalsucov  47402  reorelicc  47444  eenglngeehlnmlem1  47471  line2  47486  line2xlem  47487  itsclc0lem1  47490  itsclc0xyqsolr  47503  i0oii  47600  io1ii  47601  indthinc  47720  indthincALT  47721  setrec2fun  47785  reccot  47851  rectan  47852