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  2628  vtoclegftOLD  3555  eqeu  3677  onunel  6439  iotan0  6501  funopg  6550  dff1o2  6805  fvelimad  6928  unima  6936  fnimapr  6944  fvmptt  6988  fnreseql  7020  xpprsng  7112  f1elima  7238  f1ounsn  7247  f13dfv  7249  f1ocnvfvb  7254  f1cdmsn  7257  f1ofvswap  7281  oprssov  7558  resf1extb  7910  resf1ext2b  7911  funelss  8026  poxp  8107  poxp2  8122  poxp3  8129  smoiso  8331  oaord  8511  oaword  8513  omcan  8533  omwordri  8536  odi  8543  omeulem1  8546  oeord  8552  oecan  8553  oewordri  8556  oeordsuc  8558  nnaord  8583  nnaordr  8584  nndi  8587  nnaword  8591  nnmwordri  8600  naddel2  8652  naddss1  8653  naddss2  8654  erov  8787  ecopovtrn  8793  mapsnd  8859  f1dom3g  8939  xpdom3  9039  mapxpen  9107  dif1en  9124  dif1enOLD  9126  findcard  9127  f1domfi2  9146  entrfir  9155  domtrfil  9156  domtrfir  9158  sbthfilem  9162  sdomdomtrfi  9165  php3  9173  findcard3  9229  indexfi  9311  suppr  9423  infpr  9456  r111  9728  tcrank  9837  acndom  10004  infdif2  10162  infxpdom  10163  cfeq0  10209  cfsuc  10210  cfflb  10212  cflim2  10216  cfsmolem  10223  axcc3  10391  domtriomlem  10395  axdc3lem2  10404  axdc3lem4  10406  axdc4lem  10408  axcclem  10410  pwcfsdom  10536  tsktrss  10714  tsksuc  10715  tskuni  10736  adderpqlem  10907  mulerpqlem  10908  mulcanenq  10913  distrnq  10914  ltsonq  10922  ltanq  10924  ltmnq  10925  distrlem1pr  10978  distrlem5pr  10980  ltsopr  10985  ltsosr  11047  ltasr  11053  adddir  11165  axlttrn  11246  letr  11268  nnncan1  11458  npncan3  11460  pnpcan2  11462  subdi  11611  subdir  11612  mulcan1g  11831  mulcan2g  11832  divmul  11840  div23  11856  div13  11858  muldivdir  11875  divsubdir  11876  subdivcomb1  11877  divcan7  11891  ltmul2  12033  lemul1  12034  lemul2  12035  lemul2a  12037  lediv1  12048  ltmuldiv2  12057  lemuldiv  12063  lemuldiv2  12064  ltdiv2  12069  lediv2  12073  infrelb  12168  nndivtr  12233  bndndx  12441  nn0n0n1ge2  12510  fnn0ind  12633  addlelt  13067  xrletr  13118  qsqueeze  13161  xleadd2a  13214  xleadd1  13215  xltadd2  13217  xltmul2  13253  supxrbnd  13288  iooneg  13432  iccneg  13433  icoshft  13434  icoshftf1o  13435  zltaddlt1le  13466  fzen  13502  uzsubsubfz  13507  ssfzunsnext  13530  fzrevral2  13574  fzshftral  13576  fz0fzdiffz0  13598  elfzmlbp  13600  elfzo  13622  nelfzo  13625  fzoaddel2  13681  fzosubel2  13686  ssfzo12bi  13722  fzonfzoufzol  13731  subfzo0  13750  flltdivnn0lt  13795  modmulnn  13851  modcyc  13868  modaddabs  13873  modaddmod  13874  modmuladd  13878  modadd2mod  13886  modsubmod  13894  modsubmodmod  13895  modaddmodup  13899  modmulmod  13901  modsubdir  13905  modfzo0difsn  13908  modsumfzodifsn  13909  uzindi  13947  axdc4uzlem  13948  expneg2  14035  expdiv  14078  expubnd  14143  mulbinom2  14188  bernneq2  14195  expnngt1  14206  hashinfxadd  14350  hashunsngx  14358  hashunsnggt  14359  hashfundm  14407  hashf1dmcdm  14409  hashdifsnp1  14471  ccatval3  14544  ccatfv0  14548  ccatval1lsw  14549  ccats1val2  14592  ccatw2s1p1  14601  swrdnd  14619  pfxsuffeqwrdeq  14663  pfxsuff1eqwrdeq  14664  swrdswrd  14670  pfxpfx  14673  wrd2ind  14688  swrdccatin1  14690  pfxccatin12lem1  14693  swrdccatin2  14694  pfxccatin12lem3  14697  swrdccat  14700  pfxccatpfx1  14701  pfxccatpfx2  14702  swrdccat3blem  14704  repswswrd  14749  repswpfx  14750  repswccat  14751  cshwidxmod  14768  2cshw  14778  3cshw  14783  scshwfzeqfzo  14792  cshwcsh2id  14794  cshimadifsn  14795  cshimadifsn0  14796  ccatco  14801  cshco  14802  swrdco  14803  pfxco  14804  lswco  14805  swrds2  14906  2swrd2eqwrdeq  14919  shftuz  15035  abs3dif  15298  fsumdifsnconst  15757  modfsummods  15759  sin02gt0  16160  dvdsval2  16225  dvdscmul  16252  dvdsmulc  16253  dvdscmulr  16254  dvdsmulcr  16255  divalglem8  16370  ndvdssub  16379  dvdsexpim  16525  rpmulgcd  16527  expgcd  16533  zexpgcd  16535  coprmprod  16631  cncongr1  16637  cncongr2  16638  isprm3  16653  modprm0  16776  coprimeprodsq  16779  pythagtriplem12  16797  pythagtriplem14  16799  pcprendvds  16811  pcmul  16822  pcdiv  16823  pcqcl  16827  pcqdiv  16828  pcdvdsb  16840  vdwnnlem1  16966  hashbcss  16975  cshwshashlem1  17066  fvsetsid  17138  setsstruct2  17144  setsstruct  17146  mrcss  17577  mrcsscl  17581  mrcun  17583  cofulid  17852  catcisolem  18072  funcsetcestrclem9  18124  latleeqj1  18410  lubun  18474  clatleglb  18477  pslem  18531  dirtr  18561  mgmb1mgm1  18582  pwspjmhm  18757  grpinvid1  18923  grpinvid2  18924  grpasscan1  18933  grpasscan2  18934  grpinvadd  18950  grpsubf  18951  grpsubrcan  18953  grpinvsub  18954  grpsubeq0  18958  grpsubadd0sub  18959  grppncan  18963  grpnpcan  18964  mulgnn0p1  19017  mulgaddcomlem  19029  mulginvcom  19031  mulginvinv  19032  subgsubcl  19069  subgsub  19070  eqglact  19111  qussub  19123  ghmsub  19156  psgnunilem4  19427  oddvds2  19496  odsubdvds  19501  gexnnod  19518  slwn0  19545  dvrcl  20313  unitdvcl  20314  dvrcan1  20318  dvrcan3  20319  dvreq1  20320  rngisom1  20375  rngisomring  20376  subrgdv  20498  abvsubtri  20736  idsrngd  20765  lmodvsubval2  20823  lsmcl  20990  lsmsp2  20994  lspsntrim  21005  rngqiprngimfolem  21200  lidldvgen  21244  cncrng  21300  chrcong  21437  dvdschrmulg  21438  zndvds  21459  zntoslem  21466  ocvsscon  21584  obselocv  21637  frlmphl  21690  ascldimul  21797  mpfsubrg  22010  ply1tmcl  22158  eqcoe1ply1eq  22186  gsummoncoe1  22195  lply1binomsc  22198  mamudm  22282  mamufacex  22283  scmatf1  22418  scmatf1o  22419  scmatrngiso  22423  submabas  22465  mdetdiaglem  22485  mdetralt2  22496  mdetero  22497  mdetunilem2  22500  mdetunilem6  22504  m2detleiblem7  22514  maducoeval2  22527  gsummatr01lem3  22544  gsummatr01  22546  smadiadetglem2  22559  cramerlem1  22574  mply1topmatcl  22692  mp2pm2mplem4  22696  ntrin  22948  elnei  22998  neindisj2  23010  ordtopn3  23083  leordtval2  23099  lecldbas  23106  cnrest2  23173  cmpsublem  23286  ptrescn  23526  xkococn  23547  kqfeq  23611  snfbas  23753  neifil  23767  fclsrest  23911  utopsnnei  24137  neipcfilu  24183  psmetsym  24198  psmetge0  24200  xmetge0  24232  xmetsym  24235  metustto  24441  metustbl  24454  restmetu  24458  nm2dif  24513  nmtri  24514  cnmet  24659  cnmpopc  24822  iihalf1  24825  iihalf2  24828  iocopnst  24837  clmnegsubdi2  25005  clmsub4  25006  clmvsubval2  25010  ncvspi  25056  cphsqrtcl3  25087  cph2ass  25113  cphipval2  25141  cphipval  25143  caublcls  25209  bcthlem3  25226  bcthlem4  25227  srabn  25260  cssbn  25275  cmslsschl  25277  rrxmet  25308  rrxdsfi  25311  iblconst  25719  dvdsq1p  26068  coeid3  26145  aannenlem2  26237  pserdvlem2  26338  tanord1  26446  cxpef  26574  recxpcl  26584  logbchbase  26681  relogbcl  26683  relogbzcl  26684  logbleb  26693  logblt  26694  relogbcxpb  26697  lawcos  26726  pythag  26727  isosctrlem1  26728  isosctrlem2  26729  lgsmodeq  27253  lgsmulsqcoprm  27254  gausslemma2dlem1a  27276  2lgsoddprmlem2  27320  sltres  27574  sletr  27670  cofcutr  27832  lrrecpo  27848  sltadd2im  27893  sleadd2im  27895  sleadd1  27896  sleadd2  27897  sltadd1  27899  addscan2  27900  addscan1  27901  sltsub1  27980  divsmulw  28096  ax5seglem1  28855  axcontlem2  28892  axcontlem8  28898  upgrpredgv  29066  numedglnl  29071  issubgr2  29199  uhgrissubgr  29202  egrsubgr  29204  nbusgrfi  29301  nb3grprlem2  29308  cplgr3v  29362  cusgrsizeindslem  29379  finsumvtxdg2size  29478  rusgrpropadjvtx  29513  upgrwlkvtxedg  29573  usgr2trlncl  29690  uspgrn2crct  29738  crctcshwlkn0lem4  29743  crctcshwlkn0lem5  29744  wwlksnextproplem3  29841  umgr2adedgwlklem  29874  rusgr0edg  29903  clwwlk1loop  29917  clwwlkccatlem  29918  clwlkclwwlklem2a4  29926  clwlkclwwlklem2a  29927  clwwisshclwwslemlem  29942  erclwwlktr  29951  clwwlkel  29975  erclwwlkntr  30000  clwwlknonex2lem2  30037  uhgr3cyclex  30111  umgr3cyclex  30112  eucrctshift  30172  frgr3v  30204  3cyclfrgrrn  30215  frgrwopreglem5a  30240  frgr2wsp1  30259  extwwlkfab  30281  clwwlknonclwlknonf1o  30291  numclwwlk3lem1  30311  numclwwlk5  30317  numclwwlk6  30319  isgrpo  30426  grpoinvid1  30457  grpoinvid2  30458  grpoinvop  30462  grpodivinv  30465  grpoinvdiv  30466  grpodivf  30467  grponpcan  30472  ablonncan  30485  nvmval  30571  nvmval2  30572  nvmfval  30573  nvmul0or  30579  nvpncan2  30582  nvaddsub4  30586  nvmeq0  30587  nvdif  30595  nvpi  30596  nvmtri  30600  nvabs  30601  imsmetlem  30619  ipval2lem3  30634  ipval2  30636  4ipval2  30637  ipval3  30638  nmooge0  30696  blometi  30732  hvaddsub12  30967  hvsubdistr1  30978  hvsubdistr2  30979  hvaddcan2  31000  hvmulcan  31001  hvmulcan2  31002  hvsubcan  31003  hvsubcan2  31004  his7  31019  his2sub  31021  his2sub2  31022  norm3dif2  31080  shsubcl  31149  hhssnv  31193  shlej2  31290  fh2  31548  cm2j  31549  pjoi0  31646  hodcl  31676  hosubdi  31737  unopf1o  31845  unopadj  31848  adj2  31863  braadd  31874  bramul  31875  lnopaddmuli  31902  lnopsubmuli  31904  homco2  31906  lnfnaddmuli  31974  adjlnop  32015  leopmul  32063  leoptr  32066  pjimai  32105  atcv1  32309  atexch  32310  atcvatlem  32314  fcoinvbr  32534  preiman0  32633  divnumden2  32740  sgn3da  32759  xdivmul  32845  cshf1o  32884  resvsca  33304  idlsrgcmnd  33486  hasheuni  34075  difelsiga  34123  cndprobin  34425  bayesth  34430  signstfvp  34562  breprexplemc  34623  fineqvac  35087  swrdrevpfx  35104  swrdwlk  35114  lediv2aALT  35664  fununiq  35756  dfrdg2  35783  clsun  36316  neiin  36320  rdgeqoa  37358  curfv  37594  matunitlindflem1  37610  poimirlem32  37646  ftc1anclem4  37690  areacirc  37707  filbcmb  37734  ismtybnd  37801  grpoeqdivid  37875  ghomco  37885  rngonegrmul  37938  zerdivemp1x  37941  rngohomco  37968  rngoisoco  37976  riscer  37982  intidl  38023  isfldidl  38062  eceldmqsxrncnvepres  38398  eceldmqsxrncnvepres2  38399  brredunds  38617  lshpnelb  38977  opnlen0  39181  opcon3b  39189  opcon2b  39190  oplecon3b  39193  opltcon3b  39197  opltcon2b  39199  oldmm1  39210  oldmm4  39213  oldmj1  39214  oldmj4  39217  cvrval2  39267  cvrcon3b  39270  leatb  39285  atcmp  39304  atcvreq0  39307  atlatle  39313  athgt  39450  3dim2  39462  islln2a  39511  lplnnleat  39536  lvolnleat  39577  4atlem10  39600  4atlem11  39603  4atlem12  39606  dalem21  39688  dalem22  39689  dalem23  39690  dalem29  39695  dalem30  39696  dalem31N  39697  dalem32  39698  dalem33  39699  dalem34  39700  dalem35  39701  dalem36  39702  dalem37  39703  dalem40  39706  dalem46  39712  dalem47  39713  dalem51  39717  dalem52  39718  dalem58  39724  dalem59  39725  pmaple  39755  paddclN  39836  pmapjoin  39846  pmapjat1  39847  elpcliN  39887  pclssN  39888  pclun2N  39893  2polcon4bN  39912  paddunN  39921  poldmj1N  39922  pmapj2N  39923  pmapocjN  39924  psubclinN  39942  paddatclN  39943  poml4N  39947  lautco  40091  ldilco  40110  ltrneq2  40142  trljat1  40160  cdlemc1  40185  cdleme10  40248  ltrnco  40713  trlcocnv  40714  trljco  40734  trljco2  40735  cdlemi1  40812  tendocnv  41015  diaord  41041  dibord  41153  dihord3  41251  dihord4  41252  dihmeetlem2N  41293  dihmeetlem4preN  41300  dochdmj1  41384  hdmap10lem  41833  lcmineqlem1  42017  sticksstones2  42135  readdsub  42372  reltsub1  42374  renpncan3  42379  reppncan  42381  resubdi  42384  readdcan2  42401  mzprename  42737  dvdsrabdioph  42798  pell14qrdivcl  42853  monotoddzz  42932  jm2.19lem2  42979  jm2.19  42982  relexpaddss  43707  k0004lem3  44138  dvconstbi  44323  chordthmALT  44922  isosctrlem1ALT  44923  ssinc  45081  ssdec  45082  wessf1ornlem  45179  disjf1o  45185  ssnnf1octb  45188  projf1o  45191  mapssbi  45207  iunmapsn  45211  upbdrech  45303  iuneqfzuzlem  45330  suplesup  45335  rexabslelem  45414  climxrrelem  45747  limsupresxr  45764  liminfresxr  45765  liminfvalxr  45781  xlimliminflimsup  45860  cncfshift  45872  cncfperiod  45877  cncfuni  45884  icccncfext  45885  dvmptfprodlem  45942  dvnprodlem1  45944  itgspltprt  45977  ismbl3  45984  stoweidlem3  46001  stoweidlem10  46008  stoweidlem19  46017  stoweidlem31  46029  stoweidlem34  46032  stoweidlem44  46042  fourierdlem41  46146  fourierdlem42  46147  fourierdlem51  46155  fourierdlem68  46172  fourierdlem89  46193  fourierdlem91  46195  fourierdlem92  46196  fourierdlem94  46198  etransclem24  46256  etransclem34  46266  qndenserrnbllem  46292  salincl  46322  saldifcl2  46326  subsalsal  46357  sge0pr  46392  sge0pnffigt  46394  sge0reuz  46445  nnfoctbdjlem  46453  nnfoctbdj  46454  meadjiunlem  46463  caratheodorylem2  46525  hoidmv1le  46592  hoidmvlelem3  46595  hspmbllem2  46625  opnvonmbllem2  46631  sssmf  46736  smfaddlem1  46761  sigaraf  46851  sigarmf  46852  nltle2tri  47314  subsubelfzo0  47327  submodaddmod  47342  zplusmodne  47344  addmodne  47345  minusmod5ne  47350  submodneaddmod  47352  modmkpkne  47362  modmknepk  47363  iccpartiltu  47423  icceuelpart  47437  poprelb  47525  reuopreuprim  47527  proththd  47615  mogoldbblem  47721  fppr2odd  47732  fpprel2  47742  bgoldbtbndlem2  47807  clnbusgrfi  47843  grimuhgr  47887  uhgrimisgrgric  47931  clnbgrgrim  47934  grtrif1o  47941  grlimgrtri  47995  gpgusgralem  48047  gpgedgvtx0  48052  gpgedg2ov  48057  gpgedg2iv  48058  gpg5nbgrvtx03starlem2  48060  nn0sumltlt  48338  invginvrid  48355  ply1sclrmsm  48372  linccl  48403  lincvalpr  48407  lincresunit3lem1  48468  lincresunit3  48470  fdivmpt  48529  nnolog2flm1  48579  dignnld  48592  digexp  48596  dignn0flhalflem1  48604  itcovalsucov  48657  reorelicc  48699  eenglngeehlnmlem1  48726  line2  48741  line2xlem  48742  itsclc0lem1  48745  itsclc0xyqsolr  48758  i0oii  48908  io1ii  48909  indthinc  49451  indthincALT  49452  setrec2fun  49681  reccot  49747  rectan  49748