Theorem 3adant2 1131

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

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

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 1088

This theorem is referenced by:  3ad2ant1  1133  3simpb  1149  3imp3i2an  1346  eupickb  2630  eqeu  3660  onunel  6419  iotan0  6477  funopg  6521  dff1o2  6774  fvelimad  6895  unima  6903  fnimapr  6911  fvmptt  6955  fnreseql  6987  xpprsng  7079  f1elima  7203  f1ounsn  7212  f13dfv  7214  f1ocnvfvb  7219  f1cdmsn  7222  f1ofvswap  7246  oprssov  7521  resf1extb  7870  resf1ext2b  7871  funelss  7985  poxp  8064  poxp2  8079  poxp3  8086  smoiso  8288  oaord  8468  oaword  8470  omcan  8490  omwordri  8493  odi  8500  omeulem1  8503  oeord  8509  oecan  8510  oewordri  8513  oeordsuc  8515  nnaord  8540  nnaordr  8541  nndi  8544  nnaword  8548  nnmwordri  8557  naddel2  8609  naddss1  8610  naddss2  8611  erov  8744  ecopovtrn  8750  mapsnd  8816  f1dom3g  8896  xpdom3  8994  mapxpen  9062  dif1en  9077  findcard  9079  f1domfi2  9097  entrfir  9106  domtrfil  9107  domtrfir  9109  sbthfilem  9113  sdomdomtrfi  9116  php3  9124  findcard3  9173  indexfi  9250  suppr  9362  infpr  9395  r111  9674  tcrank  9783  acndom  9948  infdif2  10106  infxpdom  10107  cfeq0  10153  cfsuc  10154  cfflb  10156  cflim2  10160  cfsmolem  10167  axcc3  10335  domtriomlem  10339  axdc3lem2  10348  axdc3lem4  10350  axdc4lem  10352  axcclem  10354  pwcfsdom  10480  tsktrss  10658  tsksuc  10659  tskuni  10680  adderpqlem  10851  mulerpqlem  10852  mulcanenq  10857  distrnq  10858  ltsonq  10866  ltanq  10868  ltmnq  10869  distrlem1pr  10922  distrlem5pr  10924  ltsopr  10929  ltsosr  10991  ltasr  10997  adddir  11109  axlttrn  11191  letr  11213  nnncan1  11403  npncan3  11405  pnpcan2  11407  subdi  11556  subdir  11557  mulcan1g  11776  mulcan2g  11777  divmul  11785  div23  11801  div13  11803  muldivdir  11820  divsubdir  11821  subdivcomb1  11822  divcan7  11836  ltmul2  11978  lemul1  11979  lemul2  11980  lemul2a  11982  lediv1  11993  ltmuldiv2  12002  lemuldiv  12008  lemuldiv2  12009  ltdiv2  12014  lediv2  12018  infrelb  12113  nndivtr  12178  bndndx  12386  nn0n0n1ge2  12455  fnn0ind  12578  addlelt  13012  xrletr  13063  qsqueeze  13106  xleadd2a  13159  xleadd1  13160  xltadd2  13162  xltmul2  13198  supxrbnd  13233  iooneg  13377  iccneg  13378  icoshft  13379  icoshftf1o  13380  zltaddlt1le  13411  fzen  13447  uzsubsubfz  13452  ssfzunsnext  13475  fzrevral2  13519  fzshftral  13521  fz0fzdiffz0  13543  elfzmlbp  13545  elfzo  13567  nelfzo  13570  fzoaddel2  13626  fzosubel2  13631  ssfzo12bi  13667  fzonfzoufzol  13677  subfzo0  13698  flltdivnn0lt  13743  modmulnn  13799  modcyc  13816  modaddabs  13821  modaddmod  13822  modmuladd  13826  modadd2mod  13834  modsubmod  13842  modsubmodmod  13843  modaddmodup  13847  modmulmod  13849  modsubdir  13853  modfzo0difsn  13856  modsumfzodifsn  13857  uzindi  13895  axdc4uzlem  13896  expneg2  13983  expdiv  14026  expubnd  14091  mulbinom2  14136  bernneq2  14143  expnngt1  14154  hashinfxadd  14298  hashunsngx  14306  hashunsnggt  14307  hashfundm  14355  hashf1dmcdm  14357  hashdifsnp1  14419  ccatval3  14492  ccatfv0  14497  ccatval1lsw  14498  ccats1val2  14541  ccatw2s1p1  14550  swrdnd  14568  pfxsuffeqwrdeq  14611  pfxsuff1eqwrdeq  14612  swrdswrd  14618  pfxpfx  14621  wrd2ind  14636  swrdccatin1  14638  pfxccatin12lem1  14641  swrdccatin2  14642  pfxccatin12lem3  14645  swrdccat  14648  pfxccatpfx1  14649  pfxccatpfx2  14650  swrdccat3blem  14652  repswswrd  14697  repswpfx  14698  repswccat  14699  cshwidxmod  14716  2cshw  14726  3cshw  14731  scshwfzeqfzo  14739  cshwcsh2id  14741  cshimadifsn  14742  cshimadifsn0  14743  ccatco  14748  cshco  14749  swrdco  14750  pfxco  14751  lswco  14752  swrds2  14853  2swrd2eqwrdeq  14866  shftuz  14982  abs3dif  15245  fsumdifsnconst  15704  modfsummods  15706  sin02gt0  16107  dvdsval2  16172  dvdscmul  16199  dvdsmulc  16200  dvdscmulr  16201  dvdsmulcr  16202  divalglem8  16317  ndvdssub  16326  dvdsexpim  16472  rpmulgcd  16474  expgcd  16480  zexpgcd  16482  coprmprod  16578  cncongr1  16584  cncongr2  16585  isprm3  16600  modprm0  16723  coprimeprodsq  16726  pythagtriplem12  16744  pythagtriplem14  16746  pcprendvds  16758  pcmul  16769  pcdiv  16770  pcqcl  16774  pcqdiv  16775  pcdvdsb  16787  vdwnnlem1  16913  hashbcss  16922  cshwshashlem1  17013  fvsetsid  17085  setsstruct2  17091  setsstruct  17093  mrcss  17528  mrcsscl  17532  mrcun  17534  cofulid  17803  catcisolem  18023  funcsetcestrclem9  18075  latleeqj1  18363  lubun  18427  clatleglb  18430  pslem  18484  dirtr  18514  mgmb1mgm1  18569  pwspjmhm  18744  grpinvid1  18910  grpinvid2  18911  grpasscan1  18920  grpasscan2  18921  grpinvadd  18937  grpsubf  18938  grpsubrcan  18940  grpinvsub  18941  grpsubeq0  18945  grpsubadd0sub  18946  grppncan  18950  grpnpcan  18951  mulgnn0p1  19004  mulgaddcomlem  19016  mulginvcom  19018  mulginvinv  19019  subgsubcl  19056  subgsub  19057  eqglact  19097  qussub  19109  ghmsub  19142  psgnunilem4  19415  oddvds2  19484  odsubdvds  19489  gexnnod  19506  slwn0  19533  dvrcl  20328  unitdvcl  20329  dvrcan1  20333  dvrcan3  20334  dvreq1  20335  rngisom1  20390  rngisomring  20391  subrgdv  20510  abvsubtri  20748  idsrngd  20777  lmodvsubval2  20856  lsmcl  21023  lsmsp2  21027  lspsntrim  21038  rngqiprngimfolem  21233  lidldvgen  21277  cncrng  21331  chrcong  21470  dvdschrmulg  21471  zndvds  21492  zntoslem  21499  ocvsscon  21618  obselocv  21671  frlmphl  21724  ascldimul  21831  mpfsubrg  22044  ply1tmcl  22192  eqcoe1ply1eq  22220  gsummoncoe1  22229  lply1binomsc  22232  mamudm  22316  mamufacex  22317  scmatf1  22452  scmatf1o  22453  scmatrngiso  22457  submabas  22499  mdetdiaglem  22519  mdetralt2  22530  mdetero  22531  mdetunilem2  22534  mdetunilem6  22538  m2detleiblem7  22548  maducoeval2  22561  gsummatr01lem3  22578  gsummatr01  22580  smadiadetglem2  22593  cramerlem1  22608  mply1topmatcl  22726  mp2pm2mplem4  22730  ntrin  22982  elnei  23032  neindisj2  23044  ordtopn3  23117  leordtval2  23133  lecldbas  23140  cnrest2  23207  cmpsublem  23320  ptrescn  23560  xkococn  23581  kqfeq  23645  snfbas  23787  neifil  23801  fclsrest  23945  utopsnnei  24170  neipcfilu  24216  psmetsym  24231  psmetge0  24233  xmetge0  24265  xmetsym  24268  metustto  24474  metustbl  24487  restmetu  24491  nm2dif  24546  nmtri  24547  cnmet  24692  cnmpopc  24855  iihalf1  24858  iihalf2  24861  iocopnst  24870  clmnegsubdi2  25038  clmsub4  25039  clmvsubval2  25043  ncvspi  25089  cphsqrtcl3  25120  cph2ass  25146  cphipval2  25174  cphipval  25176  caublcls  25242  bcthlem3  25259  bcthlem4  25260  srabn  25293  cssbn  25308  cmslsschl  25310  rrxmet  25341  rrxdsfi  25344  iblconst  25752  dvdsq1p  26101  coeid3  26178  aannenlem2  26270  pserdvlem2  26371  tanord1  26479  cxpef  26607  recxpcl  26617  logbchbase  26714  relogbcl  26716  relogbzcl  26717  logbleb  26726  logblt  26727  relogbcxpb  26730  lawcos  26759  pythag  26760  isosctrlem1  26761  isosctrlem2  26762  lgsmodeq  27286  lgsmulsqcoprm  27287  gausslemma2dlem1a  27309  2lgsoddprmlem2  27353  sltres  27607  sletr  27703  cofcutr  27874  lrrecpo  27890  sltadd2im  27935  sleadd2im  27937  sleadd1  27938  sleadd2  27939  sltadd1  27941  addscan2  27942  addscan1  27943  sltsub1  28022  divsmulw  28138  zsoring  28338  ax5seglem1  28913  axcontlem2  28950  axcontlem8  28956  upgrpredgv  29124  numedglnl  29129  issubgr2  29257  uhgrissubgr  29260  egrsubgr  29262  nbusgrfi  29359  nb3grprlem2  29366  cplgr3v  29420  cusgrsizeindslem  29437  finsumvtxdg2size  29536  rusgrpropadjvtx  29571  upgrwlkvtxedg  29630  usgr2trlncl  29745  uspgrn2crct  29793  crctcshwlkn0lem4  29798  crctcshwlkn0lem5  29799  wwlksnextproplem3  29896  umgr2adedgwlklem  29929  rusgr0edg  29961  clwwlk1loop  29975  clwwlkccatlem  29976  clwlkclwwlklem2a4  29984  clwlkclwwlklem2a  29985  clwwisshclwwslemlem  30000  erclwwlktr  30009  clwwlkel  30033  erclwwlkntr  30058  clwwlknonex2lem2  30095  uhgr3cyclex  30169  umgr3cyclex  30170  eucrctshift  30230  frgr3v  30262  3cyclfrgrrn  30273  frgrwopreglem5a  30298  frgr2wsp1  30317  extwwlkfab  30339  clwwlknonclwlknonf1o  30349  numclwwlk3lem1  30369  numclwwlk5  30375  numclwwlk6  30377  isgrpo  30484  grpoinvid1  30515  grpoinvid2  30516  grpoinvop  30520  grpodivinv  30523  grpoinvdiv  30524  grpodivf  30525  grponpcan  30530  ablonncan  30543  nvmval  30629  nvmval2  30630  nvmfval  30631  nvmul0or  30637  nvpncan2  30640  nvaddsub4  30644  nvmeq0  30645  nvdif  30653  nvpi  30654  nvmtri  30658  nvabs  30659  imsmetlem  30677  ipval2lem3  30692  ipval2  30694  4ipval2  30695  ipval3  30696  nmooge0  30754  blometi  30790  hvaddsub12  31025  hvsubdistr1  31036  hvsubdistr2  31037  hvaddcan2  31058  hvmulcan  31059  hvmulcan2  31060  hvsubcan  31061  hvsubcan2  31062  his7  31077  his2sub  31079  his2sub2  31080  norm3dif2  31138  shsubcl  31207  hhssnv  31251  shlej2  31348  fh2  31606  cm2j  31607  pjoi0  31704  hodcl  31734  hosubdi  31795  unopf1o  31903  unopadj  31906  adj2  31921  braadd  31932  bramul  31933  lnopaddmuli  31960  lnopsubmuli  31962  homco2  31964  lnfnaddmuli  32032  adjlnop  32073  leopmul  32121  leoptr  32124  pjimai  32163  atcv1  32367  atexch  32368  atcvatlem  32372  fcoinvbr  32592  preiman0  32698  divnumden2  32805  sgn3da  32824  xdivmul  32912  cshf1o  32950  resvsca  33304  idlsrgcmnd  33487  hasheuni  34105  difelsiga  34153  cndprobin  34454  bayesth  34459  signstfvp  34591  breprexplemc  34652  trssfir1om  35129  trssfir1omregs  35139  fineqvac  35146  fineqvnttrclselem1  35148  fineqvnttrclselem3  35150  swrdrevpfx  35168  swrdwlk  35178  lediv2aALT  35728  fununiq  35820  dfrdg2  35844  clsun  36379  neiin  36383  rdgeqoa  37421  curfv  37646  matunitlindflem1  37662  poimirlem32  37698  ftc1anclem4  37742  areacirc  37759  filbcmb  37786  ismtybnd  37853  grpoeqdivid  37927  ghomco  37937  rngonegrmul  37990  zerdivemp1x  37993  rngohomco  38020  rngoisoco  38028  riscer  38034  intidl  38075  isfldidl  38114  eceldmqsxrncnvepres  38466  eceldmqsxrncnvepres2  38467  brredunds  38728  lshpnelb  39089  opnlen0  39293  opcon3b  39301  opcon2b  39302  oplecon3b  39305  opltcon3b  39309  opltcon2b  39311  oldmm1  39322  oldmm4  39325  oldmj1  39326  oldmj4  39329  cvrval2  39379  cvrcon3b  39382  leatb  39397  atcmp  39416  atcvreq0  39419  atlatle  39425  athgt  39561  3dim2  39573  islln2a  39622  lplnnleat  39647  lvolnleat  39688  4atlem10  39711  4atlem11  39714  4atlem12  39717  dalem21  39799  dalem22  39800  dalem23  39801  dalem29  39806  dalem30  39807  dalem31N  39808  dalem32  39809  dalem33  39810  dalem34  39811  dalem35  39812  dalem36  39813  dalem37  39814  dalem40  39817  dalem46  39823  dalem47  39824  dalem51  39828  dalem52  39829  dalem58  39835  dalem59  39836  pmaple  39866  paddclN  39947  pmapjoin  39957  pmapjat1  39958  elpcliN  39998  pclssN  39999  pclun2N  40004  2polcon4bN  40023  paddunN  40032  poldmj1N  40033  pmapj2N  40034  pmapocjN  40035  psubclinN  40053  paddatclN  40054  poml4N  40058  lautco  40202  ldilco  40221  ltrneq2  40253  trljat1  40271  cdlemc1  40296  cdleme10  40359  ltrnco  40824  trlcocnv  40825  trljco  40845  trljco2  40846  cdlemi1  40923  tendocnv  41126  diaord  41152  dibord  41264  dihord3  41362  dihord4  41363  dihmeetlem2N  41404  dihmeetlem4preN  41411  dochdmj1  41495  hdmap10lem  41944  lcmineqlem1  42128  sticksstones2  42246  readdsub  42483  reltsub1  42485  renpncan3  42490  reppncan  42492  resubdi  42495  readdcan2  42512  mzprename  42847  dvdsrabdioph  42908  pell14qrdivcl  42963  monotoddzz  43041  jm2.19lem2  43088  jm2.19  43091  relexpaddss  43816  k0004lem3  44247  dvconstbi  44432  chordthmALT  45030  isosctrlem1ALT  45031  ssinc  45189  ssdec  45190  wessf1ornlem  45287  disjf1o  45293  ssnnf1octb  45296  projf1o  45299  mapssbi  45315  iunmapsn  45319  upbdrech  45411  iuneqfzuzlem  45438  suplesup  45443  rexabslelem  45521  climxrrelem  45852  limsupresxr  45869  liminfresxr  45870  liminfvalxr  45886  xlimliminflimsup  45965  cncfshift  45977  cncfperiod  45982  cncfuni  45989  icccncfext  45990  dvmptfprodlem  46047  dvnprodlem1  46049  itgspltprt  46082  ismbl3  46089  stoweidlem3  46106  stoweidlem10  46113  stoweidlem19  46122  stoweidlem31  46134  stoweidlem34  46137  stoweidlem44  46147  fourierdlem41  46251  fourierdlem42  46252  fourierdlem51  46260  fourierdlem68  46277  fourierdlem89  46298  fourierdlem91  46300  fourierdlem92  46301  fourierdlem94  46303  etransclem24  46361  etransclem34  46371  qndenserrnbllem  46397  salincl  46427  saldifcl2  46431  subsalsal  46462  sge0pr  46497  sge0pnffigt  46499  sge0reuz  46550  nnfoctbdjlem  46558  nnfoctbdj  46559  meadjiunlem  46568  caratheodorylem2  46630  hoidmv1le  46697  hoidmvlelem3  46700  hspmbllem2  46730  opnvonmbllem2  46736  sssmf  46841  smfaddlem1  46866  sigaraf  46956  sigarmf  46957  nltle2tri  47418  subsubelfzo0  47431  submodaddmod  47446  zplusmodne  47448  addmodne  47449  minusmod5ne  47454  submodneaddmod  47456  modmkpkne  47466  modmknepk  47467  iccpartiltu  47527  icceuelpart  47541  poprelb  47629  reuopreuprim  47631  proththd  47719  mogoldbblem  47825  fppr2odd  47836  fpprel2  47846  bgoldbtbndlem2  47911  clnbusgrfi  47948  grimuhgr  47992  uhgrimisgrgric  48036  clnbgrgrim  48039  grtrif1o  48047  grlimgrtri  48108  gpgusgralem  48161  gpgedgvtx0  48166  gpgedg2ov  48171  gpgedg2iv  48172  gpg5nbgrvtx03starlem2  48174  nn0sumltlt  48455  invginvrid  48472  ply1sclrmsm  48489  linccl  48520  lincvalpr  48524  lincresunit3lem1  48585  lincresunit3  48587  fdivmpt  48646  nnolog2flm1  48696  dignnld  48709  digexp  48713  dignn0flhalflem1  48721  itcovalsucov  48774  reorelicc  48816  eenglngeehlnmlem1  48843  line2  48858  line2xlem  48859  itsclc0lem1  48862  itsclc0xyqsolr  48875  i0oii  49025  io1ii  49026  indthinc  49568  indthincALT  49569  setrec2fun  49798  reccot  49864  rectan  49865