Theorem 3adant2 1149

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3ad2ant1  1151  3simpb  1167  3imp3i2an  1364  eupickb  2663  eqeu  3667  onunel  6494  iotan0OLD  6554  fununiq  6581  funopg  6600  dff1o2  6858  fvelimad  6981  unima  6989  fnimapr  6997  fvmptt  7043  fnreseql  7076  xpprsng  7172  xpsnprg  7173  f1elima  7296  f1ounsn  7309  f13dfv  7311  f1ocnvfvb  7316  f1cdmsn  7319  f1ofvswap  7343  oprssov  7620  resf1extb  7978  resf1ext2b  7979  funelss  8091  poxp  8175  poxp2  8195  poxp3  8202  smoiso  8406  oaord  8591  oaword  8593  omcan  8613  omwordri  8616  odi  8623  omeulem1  8626  oeord  8633  oecan  8634  oewordri  8637  oeordsuc  8639  nnaord  8664  nnaordr  8665  nndi  8668  nnaword  8672  nnmwordri  8681  naddel2  8734  naddss1  8735  naddss2  8736  erov  8871  ecopovtrn  8877  curfv  8928  mapsnd  8950  f1dom3g  9030  xpdom3  9130  mapxpen  9198  dif1en  9213  findcard  9215  f1domfi2  9233  entrfir  9242  domtrfil  9243  domtrfir  9245  sbthfilem  9249  sdomdomtrfi  9252  php3  9260  findcard3  9310  indexfi  9385  suppr  9499  infpr  9532  r111  9817  tcrank  9936  setrec2fun  10008  acndom  10167  infdif2  10324  infxpdom  10325  cfeq0  10371  cfsuc  10372  cfflb  10374  cflim2  10378  cfsmolem  10385  axcc3  10553  domtriomlem  10557  axdc3lem2  10566  axdc3lem4  10568  axdc4lem  10570  axcclem  10572  pwcfsdom  10705  tsktrss  10883  tsksuc  10884  tskuni  10905  adderpqlem  11076  mulerpqlem  11077  mulcanenq  11082  distrnq  11083  ltsonq  11091  ltanq  11093  ltmnq  11094  distrlem1pr  11147  distrlem5pr  11149  ltsopr  11154  ltsosr  11216  ltasr  11222  adddir  11334  axlttrn  11419  nnncan1  11631  npncan3  11633  pnpcan2  11635  subdi  11786  subdir  11787  mulcan1g  12007  mulcan2g  12008  divmul  12015  div23  12031  div13  12033  muldivdir  12047  divsubdir  12048  subdivcomb1  12050  divcan7  12064  ltmul2  12206  lemul1  12207  lemul2  12208  lemul2a  12210  lediv1  12220  ltmuldiv2  12229  lemuldiv  12235  lemuldiv2  12236  ltdiv2  12241  lediv2  12245  infrelb  12340  nndivtr  12423  bndndx  12643  nn0n0n1ge2  12712  fnn0ind  12836  addlelt  13274  xrletr  13325  qsqueeze  13369  xleadd2a  13422  xleadd1  13423  xltadd2  13425  xltmul2  13461  supxrbnd  13496  iooneg  13640  iccneg  13641  icoshft  13642  icoshftf1o  13643  zltaddlt1le  13674  fzen  13712  uzsubsubfz  13718  ssfzunsnext  13741  fzrevral2  13785  fzshftral  13787  fz0fzdiffz0  13809  elfzmlbp  13811  elfzo  13833  nelfzo  13837  fzoaddel2  13893  fzosubel2  13898  ssfzo12bi  13934  fzonfzoufzol  13944  subfzo0  13966  flltdivnn0lt  14011  modmulnn  14067  modcyc  14084  modaddabs  14089  modaddmod  14090  modmuladd  14094  modadd2mod  14102  modsubmod  14110  modsubmodmod  14111  modaddmodup  14115  modmulmod  14117  modsubdir  14121  modfzo0difsn  14124  modsumfzodifsn  14125  uzindi  14163  axdc4uzlem  14164  expneg2  14251  expdiv  14294  expubnd  14359  mulbinom2  14406  bernneq2  14413  expnngt1  14424  hashinfxadd  14568  hashunsngx  14576  hashunsnggt  14577  hashfundm  14626  hashf1dmcdm  14628  hashdifsnp1  14690  ccatval3  14763  ccatfv0  14768  ccatval1lsw  14769  ccats1val2  14815  ccatw2s1p1  14824  swrdnd  14844  pfxsuffeqwrdeq  14887  pfxsuff1eqwrdeq  14888  swrdswrd  14894  pfxpfx  14897  wrd2ind  14912  swrdccatin1  14914  pfxccatin12lem1  14917  swrdccatin2  14918  pfxccatin12lem3  14921  swrdccat  14924  pfxccatpfx1  14925  pfxccatpfx2  14926  swrdccat3blem  14928  swrdrevpfx  14958  repswswrd  14975  repswpfx  14976  repswccat  14977  cshwidxmod  14994  2cshw  15004  3cshw  15009  scshwfzeqfzo  15017  cshwcsh2id  15019  cshimadifsn  15020  cshimadifsn0  15021  ccatco  15026  cshco  15027  swrdco  15028  pfxco  15029  lswco  15030  swrds2  15132  2swrd2eqwrdeq  15147  shftuz  15263  sgn3da  15295  abs3dif  15540  fsumdifsnconst  15999  modfsummods  16001  sin02gt0  16401  dvdsval2  16466  dvdscmul  16493  dvdsmulc  16494  dvdscmulr  16495  dvdsmulcr  16496  divalglem8  16611  ndvdssub  16620  dvdsexpim  16769  rpmulgcd  16772  expgcd  16778  zexpgcd  16780  coprmprod  16877  cncongr1  16883  cncongr2  16884  isprm3  16899  modprm0  17024  coprimeprodsq  17027  pythagtriplem12  17045  pythagtriplem14  17047  pcprendvds  17059  pcmul  17070  pcdiv  17071  pcqcl  17075  pcqdiv  17076  pcdvdsb  17088  vdwnnlem1  17214  hashbcss  17223  cshwshashlem1  17314  fvsetsid  17387  setsstruct2  17393  setsstruct  17395  mrcss  17831  mrcsscl  17835  mrcun  17837  cofulid  18106  catcisolem  18326  funcsetcestrclem9  18378  latleeqj1  18666  lubun  18730  clatleglb  18733  pslem  18787  dirtr  18817  mgmb1mgm1  18874  pwspjmhm  19067  grpinvid1  19243  grpinvid2  19244  grpasscan1  19253  grpasscan2  19254  grpinvadd  19269  grpsubf  19270  grpsubrcan  19272  grpinvsub  19273  grpsubeq0  19277  grpsubadd0sub  19278  grppncan  19282  grpnpcan  19283  mulgnn0p1  19336  mulgaddcomlem  19348  mulginvcom  19350  mulginvinv  19351  subgsubcl  19389  subgsub  19390  eqglact  19432  qussub  19447  ghmsub  19479  psgnunilem4  19753  oddvds2  19822  odsubdvds  19827  gexnnod  19844  slwn0  19871  dvrcl  20676  unitdvcl  20677  dvrcan1  20681  dvrcan3  20682  dvreq1  20683  rngisom1  20738  rngisomring  20739  subrgdv  20883  isdrng3lem2  21048  abvsubtri  21126  idsrngd  21155  lmodvsubval2  21234  lsmcl  21400  lsmsp2  21404  lspsntrim  21415  rngqiprngimfolem  21628  lidldvgen  21700  cncrng  21741  chrcong  21877  dvdschrmulg  21878  zndvds  21899  zntoslem  21906  ocvsscon  22025  obselocv  22078  frlmphl  22131  ascldimul  22240  mpfsubrg  22464  ply1tmcl  22635  eqcoe1ply1eq  22661  gsummoncoe1  22670  lply1binomsc  22673  mamudm  22754  mamufacex  22755  scmatf1  22890  scmatf1o  22891  scmatrngiso  22895  submabas  22937  mdetdiaglem  22957  mdetralt2  22968  mdetero  22969  mdetunilem2  22972  mdetunilem6  22976  m2detleiblem7  22986  maducoeval2  22999  gsummatr01lem3  23016  gsummatr01  23018  smadiadetglem2  23031  matunitlindflem1  23038  cramerlem1  23049  mply1topmatcl  23167  mp2pm2mplem4  23171  ntrin  23423  elnei  23473  neindisj2  23485  ordtopn3  23558  leordtval2  23574  lecldbas  23581  cnrest2  23648  cmpsublem  23761  ptrescn  24002  xkococn  24023  kqfeq  24087  snfbas  24229  neifil  24243  fclsrest  24387  utopsnnei  24612  neipcfilu  24658  psmetsym  24673  psmetge0  24675  xmetge0  24707  xmetsym  24710  metustto  24916  metustbl  24929  restmetu  24933  nm2dif  24988  nmtri  24989  cnmet  25134  cnmpopc  25293  iihalf1  25296  iihalf2  25298  iocopnst  25305  clmnegsubdi2  25470  clmsub4  25471  clmvsubval2  25475  ncvspi  25521  cphsqrtcl3  25552  cph2ass  25578  cphipval2  25606  cphipval  25608  caublcls  25674  bcthlem3  25691  bcthlem4  25692  srabn  25725  cssbn  25740  cmslsschl  25742  rrxmet  25773  rrxdsfi  25776  iblconst  26182  dvdsq1p  26525  coeid3  26603  aannenlem2  26702  pserdvlem2  26801  tanord1  26911  cxpef  27039  recxpcl  27049  logbchbase  27145  relogbcl  27147  relogbzcl  27148  logbleb  27157  logblt  27158  relogbcxpb  27161  lawcos  27190  pythag  27191  isosctrlem1  27192  isosctrlem2  27193  lgsmodeq  27715  lgsmulsqcoprm  27716  gausslemma2dlem1a  27738  2lgsoddprmlem2  27782  ltsres  28065  lestr  28165  cofcutr  28356  lrrecpo  28373  ltadds2im  28418  leadds2im  28420  leadds1  28421  leadds2  28422  ltadds1  28424  addscan2  28425  addscan1  28426  ltsubs1  28508  divmulsw  28625  oldfib  28809  zsoring  28841  bdayfinbndlem1  28899  ax5seglem1  29552  axcontlem2  29589  axcontlem8  29595  upgrpredgv  29763  numedglnl  29768  issubgr2  29899  uhgrissubgr  29902  egrsubgr  29904  nbusgrfi  30001  nb3grprlem2  30008  cplgr3v  30062  cusgrsizeindslem  30078  finsumvtxdg2size  30177  rusgrpropadjvtx  30212  upgrwlkvtxedg  30271  swrdwlk  30314  usgr2trlncl  30392  uspgrn2crct  30443  crctcshwlkn0lem4  30448  crctcshwlkn0lem5  30449  wwlksnextproplem3  30546  umgr2adedgwlklem  30579  rusgr0edg  30611  clwwlk1loop  30625  clwwlkccatlem  30626  clwlkclwwlklem2a4  30634  clwlkclwwlklem2a  30635  clwwisshclwwslemlem  30650  erclwwlktr  30659  clwwlkel  30683  erclwwlkntr  30708  clwwlknonex2lem2  30745  uhgr3cyclex  30829  umgr3cyclex  30830  eucrctshift  30890  frgr3v  30922  3cyclfrgrrn  30933  frgrwopreglem5a  30958  frgr2wsp1  30977  extwwlkfab  30999  clwwlknonclwlknonf1o  31009  numclwwlk3lem1  31029  numclwwlk5  31035  numclwwlk6  31037  isgrpo  31145  grpoinvid1  31176  grpoinvid2  31177  grpoinvop  31181  grpodivinv  31184  grpoinvdiv  31185  grpodivf  31186  grponpcan  31191  ablonncan  31204  nvmval  31290  nvmval2  31291  nvmfval  31292  nvmul0or  31298  nvpncan2  31301  nvaddsub4  31305  nvmeq0  31306  nvdif  31314  nvpi  31315  nvmtri  31319  nvabs  31320  imsmetlem  31338  ipval2lem3  31353  ipval2  31355  4ipval2  31356  ipval3  31357  nmooge0  31415  blometi  31451  hvaddsub12  31686  hvsubdistr1  31697  hvsubdistr2  31698  hvaddcan2  31719  hvmulcan  31720  hvmulcan2  31721  hvsubcan  31722  hvsubcan2  31723  his7  31738  his2sub  31740  his2sub2  31741  norm3dif2  31799  shsubcl  31868  hhssnv  31912  shlej2  32009  fh2  32267  cm2j  32268  pjoi0  32365  hodcl  32395  hosubdi  32456  unopf1o  32564  unopadj  32567  adj2  32582  braadd  32593  bramul  32594  lnopaddmuli  32621  lnopsubmuli  32623  homco2  32625  lnfnaddmuli  32693  adjlnop  32734  leopmul  32782  leoptr  32785  pjimai  32824  atcv1  33028  atexch  33029  atcvatlem  33033  fcoinvbr  33287  preiman0  33390  divnumden2  33493  xdivmul  33577  cshf1o  33609  resvsca  33990  idlsrgcmnd  34144  hasheuni  34821  cndprobin  35170  bayesth  35175  signstfvp  35304  breprexplemc  35365  f1preimaex  35819  trssfihf  35853  acwer1prclem  35885  fineqvac  35918  fineqvnttrclselem1  35923  fineqvnttrclselem3  35925  trssfihfregs  35938  lediv2aALT  36643  dfrdg2  36765  clsun  37324  neiin  37328  rdgeqoa  38554  poimirlem32  38831  ftc1anclem4  38875  areacirc  38892  filbcmb  38933  ismtybnd  39000  grpoeqdivid  39074  ghomco  39084  rngonegrmul  39137  zerdivemp1x  39140  rngohomco  39167  rngoisoco  39175  riscer  39181  intidl  39222  isfldidl  39261  eceldmqsxrncnvepres  39627  eceldmqsxrncnvepres2  39628  brredunds  39901  lshpnelb  40300  opnlen0  40504  opcon3b  40512  opcon2b  40513  oplecon3b  40516  opltcon3b  40520  opltcon2b  40522  oldmm1  40533  oldmm4  40536  oldmj1  40537  oldmj4  40540  cvrval2  40590  cvrcon3b  40593  leatb  40608  atcmp  40627  atcvreq0  40630  atlatle  40636  athgt  40772  3dim2  40784  islln2a  40833  lplnnleat  40858  lvolnleat  40899  4atlem10  40922  4atlem11  40925  4atlem12  40928  dalem21  41010  dalem22  41011  dalem23  41012  dalem29  41017  dalem30  41018  dalem31N  41019  dalem32  41020  dalem33  41021  dalem34  41022  dalem35  41023  dalem36  41024  dalem37  41025  dalem40  41028  dalem46  41034  dalem47  41035  dalem51  41039  dalem52  41040  dalem58  41046  dalem59  41047  pmaple  41077  paddclN  41158  pmapjoin  41168  pmapjat1  41169  elpcliN  41209  pclssN  41210  pclun2N  41215  2polcon4bN  41234  paddunN  41243  poldmj1N  41244  pmapj2N  41245  pmapocjN  41246  psubclinN  41264  paddatclN  41265  poml4N  41269  lautco  41413  ldilco  41432  ltrneq2  41464  trljat1  41482  cdlemc1  41507  cdleme10  41570  ltrnco  42035  trlcocnv  42036  trljco  42056  trljco2  42057  cdlemi1  42134  tendocnv  42337  diaord  42363  dibord  42475  dihord3  42573  dihord4  42574  dihmeetlem2N  42615  dihmeetlem4preN  42622  dochdmj1  42706  hdmap10lem  43155  lcmineqlem1  43338  sticksstones2  43456  readdsub  43695  reltsub1  43697  renpncan3  43702  reppncan  43704  resubdi  43707  readdcan2  43724  mzprename  44020  dvdsrabdioph  44077  pell14qrdivcl  44132  monotoddzz  44210  jm2.19lem2  44257  jm2.19  44260  relexpaddss  44973  k0004lem3  45404  dvconstbi  45573  chordthmALT  46169  isosctrlem1ALT  46170  ssinc  46369  ssdec  46370  wessf1ornlem  46467  disjf1o  46473  ssnnf1octb  46476  projf1o  46478  mapssbi  46493  iunmapsn  46497  upbdrech  46588  iuneqfzuzlem  46613  suplesup  46618  rexabslelem  46695  climxrrelem  47026  limsupresxr  47043  liminfresxr  47044  liminfvalxr  47060  xlimliminflimsup  47139  cncfshift  47151  cncfperiod  47156  cncfuni  47163  icccncfext  47164  dvmptfprodlem  47221  dvnprodlem1  47223  itgspltprt  47256  ismbl3  47263  stoweidlem3  47280  stoweidlem10  47287  stoweidlem19  47296  stoweidlem31  47308  stoweidlem34  47311  stoweidlem44  47321  fourierdlem41  47425  fourierdlem42  47426  fourierdlem51  47434  fourierdlem68  47451  fourierdlem89  47472  fourierdlem91  47474  fourierdlem92  47475  fourierdlem94  47477  etransclem24  47535  etransclem34  47545  qndenserrnbllem  47571  salincl  47601  saldifcl2  47605  subsalsal  47636  sge0pr  47671  sge0pnffigt  47673  sge0reuz  47724  nnfoctbdjlem  47732  nnfoctbdj  47733  meadjiunlem  47742  caratheodorylem2  47804  hoidmv1le  47871  hoidmvlelem3  47874  hspmbllem2  47904  opnvonmbllem2  47910  smfaddlem1  48040  sigaraf  48130  sigarmf  48131  nltle2tri  48650  subsubelfzo0  48664  nnmul2  48667  submodaddmod  48684  zplusmodne  48686  addmodne  48687  minusmod5ne  48692  submodneaddmod  48694  modmkpkne  48704  modmknepk  48705  iccpartiltu  48771  icceuelpart  48785  poprelb  48873  reuopreuprim  48875  nprmmul2  48877  proththd  48966  mogoldbblem  49085  fppr2odd  49096  fpprel2  49106  bgoldbtbndlem2  49171  clnbusgrfi  49208  grimuhgr  49252  uhgrimisgrgric  49296  clnbgrgrim  49299  grtrif1o  49307  grlimgrtri  49368  gpgusgralem  49421  gpgedgvtx0  49426  gpgedg2ov  49431  gpgedg2iv  49432  gpg5nbgrvtx03starlem2  49434  nn0sumltlt  49787  invginvrid  49804  ply1sclrmsm  49821  linccl  49851  lincvalpr  49855  lincresunit3lem1  49916  lincresunit3  49918  fdivmpt  49977  nnolog2flm1  50027  dignnld  50040  digexp  50044  dignn0flhalflem1  50052  itcovalsucov  50105  reorelicc  50147  eenglngeehlnmlem1  50175  line2  50189  line2xlem  50190  itsclc0lem1  50193  itsclc0xyqsolr  50206  i0oii  50359  io1ii  50360  indthinc  50922  indthincALT  50923  reccot  51273  rectan  51274