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  2634  vtoclegftOLD  3568  eqeu  3689  onunel  6458  iotan0  6520  funopg  6569  dff1o2  6822  fvelimad  6945  unima  6953  fnimapr  6961  fvmptt  7005  fnreseql  7037  xpprsng  7129  f1elima  7255  f1ounsn  7264  f13dfv  7266  f1ocnvfvb  7271  f1cdmsn  7274  f1ofvswap  7298  oprssov  7574  resf1extb  7928  resf1ext2b  7929  funelss  8044  poxp  8125  poxp2  8140  poxp3  8147  wfrlem4OLD  8324  smoiso  8374  oaord  8557  oaword  8559  omcan  8579  omwordri  8582  odi  8589  omeulem1  8592  oeord  8598  oecan  8599  oewordri  8602  oeordsuc  8604  nnaord  8629  nnaordr  8630  nndi  8633  nnaword  8637  nnmwordri  8646  naddel2  8698  naddss1  8699  naddss2  8700  erov  8826  ecopovtrn  8832  mapsnd  8898  f1dom3g  8980  xpdom3  9082  mapxpen  9155  dif1en  9172  dif1enOLD  9174  findcard  9175  f1domfi2  9194  entrfir  9203  domtrfil  9204  domtrfir  9206  sbthfilem  9210  sdomdomtrfi  9213  php3  9221  findcard3  9288  indexfi  9370  suppr  9482  infpr  9515  r111  9787  tcrank  9896  acndom  10063  infdif2  10221  infxpdom  10222  cfeq0  10268  cfsuc  10269  cfflb  10271  cflim2  10275  cfsmolem  10282  axcc3  10450  domtriomlem  10454  axdc3lem2  10463  axdc3lem4  10465  axdc4lem  10467  axcclem  10469  pwcfsdom  10595  tsktrss  10773  tsksuc  10774  tskuni  10795  adderpqlem  10966  mulerpqlem  10967  mulcanenq  10972  distrnq  10973  ltsonq  10981  ltanq  10983  ltmnq  10984  distrlem1pr  11037  distrlem5pr  11039  ltsopr  11044  ltsosr  11106  ltasr  11112  adddir  11224  axlttrn  11305  letr  11327  nnncan1  11517  npncan3  11519  pnpcan2  11521  subdi  11668  subdir  11669  mulcan1g  11888  mulcan2g  11889  divmul  11897  div23  11913  div13  11915  muldivdir  11932  divsubdir  11933  subdivcomb1  11934  divcan7  11948  ltmul2  12090  lemul1  12091  lemul2  12092  lemul2a  12094  lediv1  12105  ltmuldiv2  12114  lemuldiv  12120  lemuldiv2  12121  ltdiv2  12126  lediv2  12130  infrelb  12225  nndivtr  12285  bndndx  12498  nn0n0n1ge2  12567  fnn0ind  12690  addlelt  13121  xrletr  13172  qsqueeze  13215  xleadd2a  13268  xleadd1  13269  xltadd2  13271  xltmul2  13307  supxrbnd  13342  iooneg  13486  iccneg  13487  icoshft  13488  icoshftf1o  13489  zltaddlt1le  13520  fzen  13556  uzsubsubfz  13561  ssfzunsnext  13584  fzrevral2  13628  fzshftral  13630  fz0fzdiffz0  13652  elfzmlbp  13654  elfzo  13676  nelfzo  13679  fzoaddel2  13734  fzosubel2  13739  ssfzo12bi  13775  fzonfzoufzol  13784  subfzo0  13803  flltdivnn0lt  13848  modmulnn  13904  modcyc  13921  modaddabs  13924  modaddmod  13925  modmuladd  13929  modadd2mod  13937  modsubmod  13945  modsubmodmod  13946  modaddmodup  13950  modmulmod  13952  modsubdir  13956  modfzo0difsn  13959  modsumfzodifsn  13960  uzindi  13998  axdc4uzlem  13999  expneg2  14086  expdiv  14129  expubnd  14194  mulbinom2  14239  bernneq2  14246  expnngt1  14257  hashinfxadd  14401  hashunsngx  14409  hashunsnggt  14410  hashfundm  14458  hashf1dmcdm  14460  hashdifsnp1  14522  ccatval3  14595  ccatfv0  14599  ccatval1lsw  14600  ccats1val2  14643  ccatw2s1p1  14652  swrdnd  14670  pfxsuffeqwrdeq  14714  pfxsuff1eqwrdeq  14715  swrdswrd  14721  pfxpfx  14724  wrd2ind  14739  swrdccatin1  14741  pfxccatin12lem1  14744  swrdccatin2  14745  pfxccatin12lem3  14748  swrdccat  14751  pfxccatpfx1  14752  pfxccatpfx2  14753  swrdccat3blem  14755  repswswrd  14800  repswpfx  14801  repswccat  14802  cshwidxmod  14819  2cshw  14829  3cshw  14834  scshwfzeqfzo  14843  cshwcsh2id  14845  cshimadifsn  14846  cshimadifsn0  14847  ccatco  14852  cshco  14853  swrdco  14854  pfxco  14855  lswco  14856  swrds2  14957  2swrd2eqwrdeq  14970  shftuz  15086  abs3dif  15348  fsumdifsnconst  15805  modfsummods  15807  sin02gt0  16208  dvdsval2  16273  dvdscmul  16300  dvdsmulc  16301  dvdscmulr  16302  dvdsmulcr  16303  divalglem8  16417  ndvdssub  16426  dvdsexpim  16572  rpmulgcd  16574  expgcd  16580  zexpgcd  16582  coprmprod  16678  cncongr1  16684  cncongr2  16685  isprm3  16700  modprm0  16823  coprimeprodsq  16826  pythagtriplem12  16844  pythagtriplem14  16846  pcprendvds  16858  pcmul  16869  pcdiv  16870  pcqcl  16874  pcqdiv  16875  pcdvdsb  16887  vdwnnlem1  17013  hashbcss  17022  cshwshashlem1  17113  fvsetsid  17185  setsstruct2  17191  setsstruct  17193  mrcss  17626  mrcsscl  17630  mrcun  17632  cofulid  17901  catcisolem  18121  funcsetcestrclem9  18173  latleeqj1  18459  lubun  18523  clatleglb  18526  pslem  18580  dirtr  18610  mgmb1mgm1  18631  pwspjmhm  18806  grpinvid1  18972  grpinvid2  18973  grpasscan1  18982  grpasscan2  18983  grpinvadd  18999  grpsubf  19000  grpsubrcan  19002  grpinvsub  19003  grpsubeq0  19007  grpsubadd0sub  19008  grppncan  19012  grpnpcan  19013  mulgnn0p1  19066  mulgaddcomlem  19078  mulginvcom  19080  mulginvinv  19081  subgsubcl  19118  subgsub  19119  eqglact  19160  qussub  19172  ghmsub  19205  psgnunilem4  19476  oddvds2  19545  odsubdvds  19550  gexnnod  19567  slwn0  19594  dvrcl  20362  unitdvcl  20363  dvrcan1  20367  dvrcan3  20368  dvreq1  20369  rngisom1  20424  rngisomring  20425  subrgdv  20547  abvsubtri  20785  idsrngd  20814  lmodvsubval2  20872  lsmcl  21039  lsmsp2  21043  lspsntrim  21054  rngqiprngimfolem  21249  lidldvgen  21293  cncrng  21349  chrcong  21486  dvdschrmulg  21487  zndvds  21508  zntoslem  21515  ocvsscon  21633  obselocv  21686  frlmphl  21739  ascldimul  21846  mpfsubrg  22059  ply1tmcl  22207  eqcoe1ply1eq  22235  gsummoncoe1  22244  lply1binomsc  22247  mamudm  22331  mamufacex  22332  scmatf1  22467  scmatf1o  22468  scmatrngiso  22472  submabas  22514  mdetdiaglem  22534  mdetralt2  22545  mdetero  22546  mdetunilem2  22549  mdetunilem6  22553  m2detleiblem7  22563  maducoeval2  22576  gsummatr01lem3  22593  gsummatr01  22595  smadiadetglem2  22608  cramerlem1  22623  mply1topmatcl  22741  mp2pm2mplem4  22745  ntrin  22997  elnei  23047  neindisj2  23059  ordtopn3  23132  leordtval2  23148  lecldbas  23155  cnrest2  23222  cmpsublem  23335  ptrescn  23575  xkococn  23596  kqfeq  23660  snfbas  23802  neifil  23816  fclsrest  23960  utopsnnei  24186  neipcfilu  24232  psmetsym  24247  psmetge0  24249  xmetge0  24281  xmetsym  24284  metustto  24490  metustbl  24503  restmetu  24507  nm2dif  24562  nmtri  24563  cnmet  24708  cnmpopc  24871  iihalf1  24874  iihalf2  24877  iocopnst  24886  clmnegsubdi2  25054  clmsub4  25055  clmvsubval2  25059  ncvspi  25106  cphsqrtcl3  25137  cph2ass  25163  cphipval2  25191  cphipval  25193  caublcls  25259  bcthlem3  25276  bcthlem4  25277  srabn  25310  cssbn  25325  cmslsschl  25327  rrxmet  25358  rrxdsfi  25361  iblconst  25769  dvdsq1p  26118  coeid3  26195  aannenlem2  26287  pserdvlem2  26388  tanord1  26496  cxpef  26624  recxpcl  26634  logbchbase  26731  relogbcl  26733  relogbzcl  26734  logbleb  26743  logblt  26744  relogbcxpb  26747  lawcos  26776  pythag  26777  isosctrlem1  26778  isosctrlem2  26779  lgsmodeq  27303  lgsmulsqcoprm  27304  gausslemma2dlem1a  27326  2lgsoddprmlem2  27370  sltres  27624  sletr  27720  cofcutr  27875  lrrecpo  27891  sltadd2im  27936  sleadd2im  27938  sleadd1  27939  sleadd2  27940  sltadd1  27942  addscan2  27943  addscan1  27944  sltsub1  28023  divsmulw  28135  ax5seglem1  28853  axcontlem2  28890  axcontlem8  28896  upgrpredgv  29064  numedglnl  29069  issubgr2  29197  uhgrissubgr  29200  egrsubgr  29202  nbusgrfi  29299  nb3grprlem2  29306  cplgr3v  29360  cusgrsizeindslem  29377  finsumvtxdg2size  29476  rusgrpropadjvtx  29511  upgrwlkvtxedg  29571  usgr2trlncl  29688  uspgrn2crct  29736  crctcshwlkn0lem4  29741  crctcshwlkn0lem5  29742  wwlksnextproplem3  29839  umgr2adedgwlklem  29872  rusgr0edg  29901  clwwlk1loop  29915  clwwlkccatlem  29916  clwlkclwwlklem2a4  29924  clwlkclwwlklem2a  29925  clwwisshclwwslemlem  29940  erclwwlktr  29949  clwwlkel  29973  erclwwlkntr  29998  clwwlknonex2lem2  30035  uhgr3cyclex  30109  umgr3cyclex  30110  eucrctshift  30170  frgr3v  30202  3cyclfrgrrn  30213  frgrwopreglem5a  30238  frgr2wsp1  30257  extwwlkfab  30279  clwwlknonclwlknonf1o  30289  numclwwlk3lem1  30309  numclwwlk5  30315  numclwwlk6  30317  isgrpo  30424  grpoinvid1  30455  grpoinvid2  30456  grpoinvop  30460  grpodivinv  30463  grpoinvdiv  30464  grpodivf  30465  grponpcan  30470  ablonncan  30483  nvmval  30569  nvmval2  30570  nvmfval  30571  nvmul0or  30577  nvpncan2  30580  nvaddsub4  30584  nvmeq0  30585  nvdif  30593  nvpi  30594  nvmtri  30598  nvabs  30599  imsmetlem  30617  ipval2lem3  30632  ipval2  30634  4ipval2  30635  ipval3  30636  nmooge0  30694  blometi  30730  hvaddsub12  30965  hvsubdistr1  30976  hvsubdistr2  30977  hvaddcan2  30998  hvmulcan  30999  hvmulcan2  31000  hvsubcan  31001  hvsubcan2  31002  his7  31017  his2sub  31019  his2sub2  31020  norm3dif2  31078  shsubcl  31147  hhssnv  31191  shlej2  31288  fh2  31546  cm2j  31547  pjoi0  31644  hodcl  31674  hosubdi  31735  unopf1o  31843  unopadj  31846  adj2  31861  braadd  31872  bramul  31873  lnopaddmuli  31900  lnopsubmuli  31902  homco2  31904  lnfnaddmuli  31972  adjlnop  32013  leopmul  32061  leoptr  32064  pjimai  32103  atcv1  32307  atexch  32308  atcvatlem  32312  fcoinvbr  32532  preiman0  32633  divnumden2  32740  sgn3da  32759  xdivmul  32845  cshf1o  32884  resvsca  33294  idlsrgcmnd  33476  hasheuni  34062  difelsiga  34110  cndprobin  34412  bayesth  34417  signstfvp  34549  breprexplemc  34610  fineqvac  35074  swrdrevpfx  35085  swrdwlk  35095  lediv2aALT  35645  fununiq  35732  dfrdg2  35759  clsun  36292  neiin  36296  rdgeqoa  37334  curfv  37570  matunitlindflem1  37586  poimirlem32  37622  ftc1anclem4  37666  areacirc  37683  filbcmb  37710  ismtybnd  37777  grpoeqdivid  37851  ghomco  37861  rngonegrmul  37914  zerdivemp1x  37917  rngohomco  37944  rngoisoco  37952  riscer  37958  intidl  37999  isfldidl  38038  brredunds  38590  lshpnelb  38948  opnlen0  39152  opcon3b  39160  opcon2b  39161  oplecon3b  39164  opltcon3b  39168  opltcon2b  39170  oldmm1  39181  oldmm4  39184  oldmj1  39185  oldmj4  39188  cvrval2  39238  cvrcon3b  39241  leatb  39256  atcmp  39275  atcvreq0  39278  atlatle  39284  athgt  39421  3dim2  39433  islln2a  39482  lplnnleat  39507  lvolnleat  39548  4atlem10  39571  4atlem11  39574  4atlem12  39577  dalem21  39659  dalem22  39660  dalem23  39661  dalem29  39666  dalem30  39667  dalem31N  39668  dalem32  39669  dalem33  39670  dalem34  39671  dalem35  39672  dalem36  39673  dalem37  39674  dalem40  39677  dalem46  39683  dalem47  39684  dalem51  39688  dalem52  39689  dalem58  39695  dalem59  39696  pmaple  39726  paddclN  39807  pmapjoin  39817  pmapjat1  39818  elpcliN  39858  pclssN  39859  pclun2N  39864  2polcon4bN  39883  paddunN  39892  poldmj1N  39893  pmapj2N  39894  pmapocjN  39895  psubclinN  39913  paddatclN  39914  poml4N  39918  lautco  40062  ldilco  40081  ltrneq2  40113  trljat1  40131  cdlemc1  40156  cdleme10  40219  ltrnco  40684  trlcocnv  40685  trljco  40705  trljco2  40706  cdlemi1  40783  tendocnv  40986  diaord  41012  dibord  41124  dihord3  41222  dihord4  41223  dihmeetlem2N  41264  dihmeetlem4preN  41271  dochdmj1  41355  hdmap10lem  41804  lcmineqlem1  41988  sticksstones2  42106  metakunt29  42192  metakunt30  42193  factwoffsmonot  42201  readdsub  42374  reltsub1  42376  renpncan3  42381  reppncan  42383  resubdi  42386  readdcan2  42402  mzprename  42719  dvdsrabdioph  42780  pell14qrdivcl  42835  monotoddzz  42914  jm2.19lem2  42961  jm2.19  42964  relexpaddss  43689  k0004lem3  44120  dvconstbi  44306  chordthmALT  44905  isosctrlem1ALT  44906  ssinc  45059  ssdec  45060  wessf1ornlem  45157  disjf1o  45163  ssnnf1octb  45166  projf1o  45169  mapssbi  45185  iunmapsn  45189  upbdrech  45282  iuneqfzuzlem  45309  suplesup  45314  rexabslelem  45393  climxrrelem  45726  limsupresxr  45743  liminfresxr  45744  liminfvalxr  45760  xlimliminflimsup  45839  cncfshift  45851  cncfperiod  45856  cncfuni  45863  icccncfext  45864  dvmptfprodlem  45921  dvnprodlem1  45923  itgspltprt  45956  ismbl3  45963  stoweidlem3  45980  stoweidlem10  45987  stoweidlem19  45996  stoweidlem31  46008  stoweidlem34  46011  stoweidlem44  46021  fourierdlem41  46125  fourierdlem42  46126  fourierdlem51  46134  fourierdlem68  46151  fourierdlem89  46172  fourierdlem91  46174  fourierdlem92  46175  fourierdlem94  46177  etransclem24  46235  etransclem34  46245  qndenserrnbllem  46271  salincl  46301  saldifcl2  46305  subsalsal  46336  sge0pr  46371  sge0pnffigt  46373  sge0reuz  46424  nnfoctbdjlem  46432  nnfoctbdj  46433  meadjiunlem  46442  caratheodorylem2  46504  hoidmv1le  46571  hoidmvlelem3  46574  hspmbllem2  46604  opnvonmbllem2  46610  sssmf  46715  smfaddlem1  46740  sigaraf  46830  sigarmf  46831  nltle2tri  47290  subsubelfzo0  47303  submodaddmod  47318  zplusmodne  47320  addmodne  47321  minusmod5ne  47326  submodneaddmod  47328  iccpartiltu  47384  icceuelpart  47398  poprelb  47486  reuopreuprim  47488  proththd  47576  mogoldbblem  47682  fppr2odd  47693  fpprel2  47703  bgoldbtbndlem2  47768  clnbusgrfi  47804  grimuhgr  47848  uhgrimisgrgric  47892  clnbgrgrim  47895  grtrif1o  47902  grlimgrtri  47956  gpgusgralem  48008  gpgedgvtx0  48013  gpg5nbgrvtx03starlem2  48019  nn0sumltlt  48273  invginvrid  48290  ply1sclrmsm  48307  linccl  48338  lincvalpr  48342  lincresunit3lem1  48403  lincresunit3  48405  fdivmpt  48468  nnolog2flm1  48518  dignnld  48531  digexp  48535  dignn0flhalflem1  48543  itcovalsucov  48596  reorelicc  48638  eenglngeehlnmlem1  48665  line2  48680  line2xlem  48681  itsclc0lem1  48684  itsclc0xyqsolr  48697  i0oii  48842  io1ii  48843  indthinc  49296  indthincALT  49297  setrec2fun  49504  reccot  49570  rectan  49571