Theorem 3adant2 1129

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

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

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 396  df-3an 1087

This theorem is referenced by:  3ad2ant1  1131  3simpb  1147  3imp3i2an  1343  eupickb  2637  vtoclegft  3512  eqeu  3636  iotan0  6408  funopg  6452  fncoOLD  6534  dff1o2  6705  fvelimad  6818  unima  6825  fnimapr  6834  fvmptt  6877  fnreseql  6907  xpprsng  6994  f1elima  7117  f13dfv  7127  f1ocnvfvb  7132  f1ofvswap  7158  oprssov  7419  funelss  7861  poxp  7940  wfrlem4OLD  8114  smoiso  8164  oaord  8340  oaword  8342  omcan  8362  omwordri  8365  odi  8372  omeulem1  8375  oeord  8381  oecan  8382  oewordri  8385  oeordsuc  8387  nnaord  8412  nnaordr  8413  nndi  8416  nnaword  8420  nnmwordri  8429  erov  8561  ecopovtrn  8567  mapsnd  8632  f1dom3g  8710  xpdom3  8810  mapxpen  8879  dif1en  8907  findcard  8908  entrfir  8937  domtrfi  8938  sbthfilem  8941  indexfi  9057  suppr  9160  infpr  9192  r111  9464  tcrank  9573  acndom  9738  infdif2  9897  infxpdom  9898  cfeq0  9943  cfsuc  9944  cfflb  9946  cflim2  9950  cfsmolem  9957  axcc3  10125  domtriomlem  10129  axdc3lem2  10138  axdc3lem4  10140  axdc4lem  10142  axcclem  10144  pwcfsdom  10270  tsktrss  10448  tsksuc  10449  tskuni  10470  adderpqlem  10641  mulerpqlem  10642  mulcanenq  10647  distrnq  10648  ltsonq  10656  ltanq  10658  ltmnq  10659  distrlem1pr  10712  distrlem5pr  10714  ltsopr  10719  ltsosr  10781  ltasr  10787  adddir  10897  axlttrn  10978  letr  10999  nnncan1  11187  npncan3  11189  pnpcan2  11191  subdi  11338  subdir  11339  mulcan1g  11558  mulcan2g  11559  divmul  11566  div23  11582  div13  11584  muldivdir  11598  divsubdir  11599  subdivcomb1  11600  divcan7  11614  ltmul2  11756  lemul1  11757  lemul2  11758  lemul2a  11760  lediv1  11770  ltmuldiv2  11779  lemuldiv  11785  lemuldiv2  11786  ltdiv2  11791  lediv2  11795  infrelb  11890  nndivtr  11950  bndndx  12162  nn0n0n1ge2  12230  fnn0ind  12349  addlelt  12773  xrletr  12821  qsqueeze  12864  xleadd2a  12917  xleadd1  12918  xltadd2  12920  xltmul2  12956  supxrbnd  12991  iooneg  13132  iccneg  13133  icoshft  13134  icoshftf1o  13135  zltaddlt1le  13166  fzen  13202  uzsubsubfz  13207  ssfzunsnext  13230  fzrevral2  13271  fzshftral  13273  fz0fzdiffz0  13294  elfzmlbp  13296  elfzo  13318  nelfzo  13321  fzoaddel2  13371  fzosubel2  13375  ssfzo12bi  13410  fzonfzoufzol  13418  subfzo0  13437  flltdivnn0lt  13481  modmulnn  13537  modcyc  13554  modaddabs  13557  modaddmod  13558  modmuladd  13561  modadd2mod  13569  modsubmod  13577  modsubmodmod  13578  modaddmodup  13582  modmulmod  13584  modsubdir  13588  modfzo0difsn  13591  modsumfzodifsn  13592  uzindi  13630  axdc4uzlem  13631  expneg2  13719  expdiv  13762  expubnd  13823  mulbinom2  13866  bernneq2  13873  expnngt1  13884  hashinfxadd  14028  hashunsngx  14036  hashunsnggt  14037  hashdifsnp1  14138  ccatval3  14212  ccatfv0  14216  ccatval1lsw  14217  ccats1val2  14262  ccatw2s1p1  14274  swrdnd  14295  pfxsuffeqwrdeq  14339  pfxsuff1eqwrdeq  14340  swrdswrd  14346  pfxpfx  14349  wrd2ind  14364  swrdccatin1  14366  pfxccatin12lem1  14369  swrdccatin2  14370  pfxccatin12lem3  14373  swrdccat  14376  pfxccatpfx1  14377  pfxccatpfx2  14378  swrdccat3blem  14380  repswswrd  14425  repswpfx  14426  repswccat  14427  cshwidxmod  14444  2cshw  14454  3cshw  14459  scshwfzeqfzo  14467  cshwcsh2id  14469  cshimadifsn  14470  cshimadifsn0  14471  ccatco  14476  cshco  14477  swrdco  14478  pfxco  14479  lswco  14480  swrds2  14581  2swrd2eqwrdeq  14594  shftuz  14708  abs3dif  14971  fsumdifsnconst  15431  modfsummods  15433  sin02gt0  15829  dvdsval2  15894  dvdscmul  15920  dvdsmulc  15921  dvdscmulr  15922  dvdsmulcr  15923  divalglem8  16037  ndvdssub  16046  rpmulgcd  16194  coprmprod  16294  cncongr1  16300  cncongr2  16301  isprm3  16316  modprm0  16434  coprimeprodsq  16437  pythagtriplem12  16455  pythagtriplem14  16457  pcprendvds  16469  pcmul  16480  pcdiv  16481  pcqcl  16485  pcqdiv  16486  pcdvdsb  16498  vdwnnlem1  16624  hashbcss  16633  cshwshashlem1  16725  fvsetsid  16797  setsstruct2  16803  setsstruct  16805  mrcss  17242  mrcsscl  17246  mrcun  17248  cofulid  17521  catcisolem  17741  funcsetcestrclem9  17796  latleeqj1  18084  lubun  18148  clatleglb  18151  pslem  18205  dirtr  18235  mgmb1mgm1  18254  pwspjmhm  18383  grpinvid1  18545  grpinvid2  18546  grpasscan1  18553  grpasscan2  18554  grpinvadd  18568  grpsubf  18569  grpsubrcan  18571  grpinvsub  18572  grpsubeq0  18576  grpsubadd0sub  18577  grppncan  18581  grpnpcan  18582  mulgnn0p1  18630  mulgaddcomlem  18641  mulginvcom  18643  mulginvinv  18644  subgsubcl  18681  subgsub  18682  eqglact  18722  qussub  18731  ghmsub  18757  psgnunilem4  19020  oddvds2  19088  odsubdvds  19091  gexnnod  19108  slwn0  19135  dvrcl  19843  unitdvcl  19844  dvrcan1  19848  dvrcan3  19849  dvreq1  19850  subrgdv  19956  abvsubtri  20010  idsrngd  20037  lmodvsubval2  20093  lsmcl  20260  lsmsp2  20264  lspsntrim  20275  lidldvgen  20439  chrcong  20645  zndvds  20669  zntoslem  20676  ocvsscon  20792  obselocv  20845  frlmphl  20898  ascldimul  21002  mpfsubrg  21223  ply1tmcl  21353  eqcoe1ply1eq  21378  gsummoncoe1  21385  lply1binomsc  21388  mamudm  21447  mamufacex  21448  scmatf1  21588  scmatf1o  21589  scmatrngiso  21593  submabas  21635  mdetdiaglem  21655  mdetralt2  21666  mdetero  21667  mdetunilem2  21670  mdetunilem6  21674  m2detleiblem7  21684  maducoeval2  21697  gsummatr01lem3  21714  gsummatr01  21716  smadiadetglem2  21729  cramerlem1  21744  mply1topmatcl  21862  mp2pm2mplem4  21866  ntrin  22120  elnei  22170  neindisj2  22182  ordtopn3  22255  leordtval2  22271  lecldbas  22278  cnrest2  22345  cmpsublem  22458  ptrescn  22698  xkococn  22719  kqfeq  22783  snfbas  22925  neifil  22939  fclsrest  23083  utopsnnei  23309  neipcfilu  23356  psmetsym  23371  psmetge0  23373  xmetge0  23405  xmetsym  23408  metustto  23615  metustbl  23628  restmetu  23632  nm2dif  23687  nmtri  23688  cnmet  23841  cnmpopc  23997  iihalf1  24000  iihalf2  24002  iocopnst  24009  clmnegsubdi2  24174  clmsub4  24175  clmvsubval2  24179  ncvspi  24225  cphsqrtcl3  24256  cph2ass  24282  cphipval2  24310  cphipval  24312  caublcls  24378  bcthlem3  24395  bcthlem4  24396  srabn  24429  cssbn  24444  cmslsschl  24446  rrxmet  24477  rrxdsfi  24480  iblconst  24887  tdeglem3OLD  25128  dvdsq1p  25230  coeid3  25306  aannenlem2  25394  pserdvlem2  25492  tanord1  25598  cxpef  25725  recxpcl  25735  logbchbase  25826  relogbcl  25828  relogbzcl  25829  logbleb  25838  logblt  25839  relogbcxpb  25842  lawcos  25871  pythag  25872  isosctrlem1  25873  isosctrlem2  25874  lgsmodeq  26395  lgsmulsqcoprm  26396  gausslemma2dlem1a  26418  2lgsoddprmlem2  26462  ax5seglem1  27199  axcontlem2  27236  axcontlem8  27242  upgrpredgv  27412  numedglnl  27417  issubgr2  27542  uhgrissubgr  27545  egrsubgr  27547  nbusgrfi  27644  nb3grprlem2  27651  cplgr3v  27705  cusgrsizeindslem  27721  finsumvtxdg2size  27820  rusgrpropadjvtx  27855  upgrwlkvtxedg  27914  usgr2trlncl  28029  uspgrn2crct  28074  crctcshwlkn0lem4  28079  crctcshwlkn0lem5  28080  wwlksnextproplem3  28177  umgr2adedgwlklem  28210  rusgr0edg  28239  clwwlk1loop  28253  clwwlkccatlem  28254  clwlkclwwlklem2a4  28262  clwlkclwwlklem2a  28263  clwwisshclwwslemlem  28278  erclwwlktr  28287  clwwlkel  28311  erclwwlkntr  28336  clwwlknonex2lem2  28373  uhgr3cyclex  28447  umgr3cyclex  28448  eucrctshift  28508  frgr3v  28540  3cyclfrgrrn  28551  frgrwopreglem5a  28576  frgr2wsp1  28595  extwwlkfab  28617  clwwlknonclwlknonf1o  28627  numclwwlk3lem1  28647  numclwwlk5  28653  numclwwlk6  28655  isgrpo  28760  grpoinvid1  28791  grpoinvid2  28792  grpoinvop  28796  grpodivinv  28799  grpoinvdiv  28800  grpodivf  28801  grponpcan  28806  ablonncan  28819  nvmval  28905  nvmval2  28906  nvmfval  28907  nvmul0or  28913  nvpncan2  28916  nvaddsub4  28920  nvmeq0  28921  nvdif  28929  nvpi  28930  nvmtri  28934  nvabs  28935  imsmetlem  28953  ipval2lem3  28968  ipval2  28970  4ipval2  28971  ipval3  28972  nmooge0  29030  blometi  29066  hvaddsub12  29301  hvsubdistr1  29312  hvsubdistr2  29313  hvaddcan2  29334  hvmulcan  29335  hvmulcan2  29336  hvsubcan  29337  hvsubcan2  29338  his7  29353  his2sub  29355  his2sub2  29356  norm3dif2  29414  shsubcl  29483  hhssnv  29527  shlej2  29624  fh2  29882  cm2j  29883  pjoi0  29980  hodcl  30010  hosubdi  30071  unopf1o  30179  unopadj  30182  adj2  30197  braadd  30208  bramul  30209  lnopaddmuli  30236  lnopsubmuli  30238  homco2  30240  lnfnaddmuli  30308  adjlnop  30349  leopmul  30397  leoptr  30400  pjimai  30439  atcv1  30643  atexch  30644  atcvatlem  30648  fcoinvbr  30848  preiman0  30944  divnumden2  31034  xdivmul  31101  cshf1o  31136  dvdschrmulg  31385  resvsca  31431  idlsrgcmnd  31562  hasheuni  31953  difelsiga  32001  cndprobin  32301  bayesth  32306  sgn3da  32408  signstfvp  32450  breprexplemc  32512  fineqvac  32966  hashfundm  32974  hashf1dmcdm  32976  swrdrevpfx  32978  swrdwlk  32988  lediv2aALT  33535  onunel  33592  fununiq  33649  dfrdg2  33677  poxp2  33717  poxp3  33723  naddel2  33767  naddss1  33768  naddss2  33769  sltres  33792  sletr  33888  cofcutr  34019  lrrecpo  34025  clsun  34444  neiin  34448  rdgeqoa  35468  curfv  35684  matunitlindflem1  35700  poimirlem32  35736  ftc1anclem4  35780  areacirc  35797  filbcmb  35825  ismtybnd  35892  grpoeqdivid  35966  ghomco  35976  rngonegrmul  36029  zerdivemp1x  36032  rngohomco  36059  rngoisoco  36067  riscer  36073  intidl  36114  isfldidl  36153  brredunds  36666  lshpnelb  36925  opnlen0  37129  opcon3b  37137  opcon2b  37138  oplecon3b  37141  opltcon3b  37145  opltcon2b  37147  oldmm1  37158  oldmm4  37161  oldmj1  37162  oldmj4  37165  cvrval2  37215  cvrcon3b  37218  leatb  37233  atcmp  37252  atcvreq0  37255  atlatle  37261  athgt  37397  3dim2  37409  islln2a  37458  lplnnleat  37483  lvolnleat  37524  4atlem10  37547  4atlem11  37550  4atlem12  37553  dalem21  37635  dalem22  37636  dalem23  37637  dalem29  37642  dalem30  37643  dalem31N  37644  dalem32  37645  dalem33  37646  dalem34  37647  dalem35  37648  dalem36  37649  dalem37  37650  dalem40  37653  dalem46  37659  dalem47  37660  dalem51  37664  dalem52  37665  dalem58  37671  dalem59  37672  pmaple  37702  paddclN  37783  pmapjoin  37793  pmapjat1  37794  elpcliN  37834  pclssN  37835  pclun2N  37840  2polcon4bN  37859  paddunN  37868  poldmj1N  37869  pmapj2N  37870  pmapocjN  37871  psubclinN  37889  paddatclN  37890  poml4N  37894  lautco  38038  ldilco  38057  ltrneq2  38089  trljat1  38107  cdlemc1  38132  cdleme10  38195  ltrnco  38660  trlcocnv  38661  trljco  38681  trljco2  38682  cdlemi1  38759  tendocnv  38962  diaord  38988  dibord  39100  dihord3  39198  dihord4  39199  dihmeetlem2N  39240  dihmeetlem4preN  39247  dochdmj1  39331  hdmap10lem  39780  lcmineqlem1  39965  sticksstones2  40031  metakunt29  40081  metakunt30  40082  factwoffsmonot  40091  dvdsexpim  40249  expgcd  40255  zexpgcd  40257  readdsub  40288  reltsub1  40290  renpncan3  40295  reppncan  40297  resubdi  40300  readdcan2  40316  mzprename  40487  dvdsrabdioph  40548  pell14qrdivcl  40603  monotoddzz  40681  jm2.19lem2  40728  jm2.19  40731  relexpaddss  41215  k0004lem3  41648  dvconstbi  41841  chordthmALT  42442  isosctrlem1ALT  42443  ssinc  42526  ssdec  42527  wessf1ornlem  42611  disjf1o  42618  ssnnf1octb  42622  projf1o  42625  mapssbi  42642  iunmapsn  42646  upbdrech  42734  iuneqfzuzlem  42763  suplesup  42768  rexabslelem  42848  climxrrelem  43180  limsupresxr  43197  liminfresxr  43198  liminfvalxr  43214  xlimliminflimsup  43293  cncfshift  43305  cncfperiod  43310  cncfuni  43317  icccncfext  43318  dvmptfprodlem  43375  dvnprodlem1  43377  itgspltprt  43410  ismbl3  43417  stoweidlem3  43434  stoweidlem10  43441  stoweidlem19  43450  stoweidlem31  43462  stoweidlem34  43465  stoweidlem44  43475  fourierdlem41  43579  fourierdlem42  43580  fourierdlem51  43588  fourierdlem68  43605  fourierdlem89  43626  fourierdlem91  43628  fourierdlem92  43629  fourierdlem94  43631  etransclem24  43689  etransclem34  43699  qndenserrnbllem  43725  salincl  43754  saldifcl2  43757  subsalsal  43788  sge0pr  43822  sge0pnffigt  43824  sge0reuz  43875  nnfoctbdjlem  43883  nnfoctbdj  43884  meadjiunlem  43893  caratheodorylem2  43955  hoidmv1le  44022  hoidmvlelem3  44025  hspmbllem2  44055  opnvonmbllem2  44061  sssmf  44161  smfaddlem1  44185  sigaraf  44256  sigarmf  44257  nltle2tri  44693  subsubelfzo0  44706  iccpartiltu  44762  icceuelpart  44776  poprelb  44864  reuopreuprim  44866  proththd  44954  mogoldbblem  45060  fppr2odd  45071  fpprel2  45081  bgoldbtbndlem2  45146  isomgrtr  45179  nn0sumltlt  45574  invginvrid  45591  ply1sclrmsm  45612  linccl  45643  lincvalpr  45647  lincresunit3lem1  45708  lincresunit3  45710  fdivmpt  45774  nnolog2flm1  45824  dignnld  45837  digexp  45841  dignn0flhalflem1  45849  itcovalsucov  45902  reorelicc  45944  eenglngeehlnmlem1  45971  line2  45986  line2xlem  45987  itsclc0lem1  45990  itsclc0xyqsolr  46003  i0oii  46101  io1ii  46102  indthinc  46221  indthincALT  46222  setrec2fun  46284  reccot  46346  rectan  46347