Theorem 3adant2 1130

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  1132  3simpb  1148  3imp3i2an  1344  eupickb  2632  vtoclegftOLD  3588  eqeu  3714  onunel  6490  iotan0  6552  funopg  6601  dff1o2  6853  fvelimad  6975  unima  6983  fnimapr  6991  fvmptt  7035  fnreseql  7067  xpprsng  7159  f1elima  7282  f1ounsn  7291  f13dfv  7293  f1ocnvfvb  7298  f1cdmsn  7301  f1ofvswap  7325  oprssov  7601  funelss  8070  poxp  8151  poxp2  8166  poxp3  8173  wfrlem4OLD  8350  smoiso  8400  oaord  8583  oaword  8585  omcan  8605  omwordri  8608  odi  8615  omeulem1  8618  oeord  8624  oecan  8625  oewordri  8628  oeordsuc  8630  nnaord  8655  nnaordr  8656  nndi  8659  nnaword  8663  nnmwordri  8672  naddel2  8724  naddss1  8725  naddss2  8726  erov  8852  ecopovtrn  8858  mapsnd  8924  f1dom3g  9006  xpdom3  9108  mapxpen  9181  dif1en  9198  dif1enOLD  9200  findcard  9201  f1domfi2  9219  entrfir  9228  domtrfil  9229  domtrfir  9231  sbthfilem  9235  sdomdomtrfi  9238  php3  9246  findcard3  9315  indexfi  9397  suppr  9508  infpr  9540  r111  9812  tcrank  9921  acndom  10088  infdif2  10246  infxpdom  10247  cfeq0  10293  cfsuc  10294  cfflb  10296  cflim2  10300  cfsmolem  10307  axcc3  10475  domtriomlem  10479  axdc3lem2  10488  axdc3lem4  10490  axdc4lem  10492  axcclem  10494  pwcfsdom  10620  tsktrss  10798  tsksuc  10799  tskuni  10820  adderpqlem  10991  mulerpqlem  10992  mulcanenq  10997  distrnq  10998  ltsonq  11006  ltanq  11008  ltmnq  11009  distrlem1pr  11062  distrlem5pr  11064  ltsopr  11069  ltsosr  11131  ltasr  11137  adddir  11249  axlttrn  11330  letr  11352  nnncan1  11542  npncan3  11544  pnpcan2  11546  subdi  11693  subdir  11694  mulcan1g  11913  mulcan2g  11914  divmul  11922  div23  11938  div13  11940  muldivdir  11957  divsubdir  11958  subdivcomb1  11959  divcan7  11973  ltmul2  12115  lemul1  12116  lemul2  12117  lemul2a  12119  lediv1  12130  ltmuldiv2  12139  lemuldiv  12145  lemuldiv2  12146  ltdiv2  12151  lediv2  12155  infrelb  12250  nndivtr  12310  bndndx  12522  nn0n0n1ge2  12591  fnn0ind  12714  addlelt  13146  xrletr  13196  qsqueeze  13239  xleadd2a  13292  xleadd1  13293  xltadd2  13295  xltmul2  13331  supxrbnd  13366  iooneg  13507  iccneg  13508  icoshft  13509  icoshftf1o  13510  zltaddlt1le  13541  fzen  13577  uzsubsubfz  13582  ssfzunsnext  13605  fzrevral2  13649  fzshftral  13651  fz0fzdiffz0  13673  elfzmlbp  13675  elfzo  13697  nelfzo  13700  fzoaddel2  13755  fzosubel2  13760  ssfzo12bi  13796  fzonfzoufzol  13805  subfzo0  13824  flltdivnn0lt  13869  modmulnn  13925  modcyc  13942  modaddabs  13945  modaddmod  13946  modmuladd  13950  modadd2mod  13958  modsubmod  13966  modsubmodmod  13967  modaddmodup  13971  modmulmod  13973  modsubdir  13977  modfzo0difsn  13980  modsumfzodifsn  13981  uzindi  14019  axdc4uzlem  14020  expneg2  14107  expdiv  14150  expubnd  14213  mulbinom2  14258  bernneq2  14265  expnngt1  14276  hashinfxadd  14420  hashunsngx  14428  hashunsnggt  14429  hashfundm  14477  hashf1dmcdm  14479  hashdifsnp1  14541  ccatval3  14613  ccatfv0  14617  ccatval1lsw  14618  ccats1val2  14661  ccatw2s1p1  14670  swrdnd  14688  pfxsuffeqwrdeq  14732  pfxsuff1eqwrdeq  14733  swrdswrd  14739  pfxpfx  14742  wrd2ind  14757  swrdccatin1  14759  pfxccatin12lem1  14762  swrdccatin2  14763  pfxccatin12lem3  14766  swrdccat  14769  pfxccatpfx1  14770  pfxccatpfx2  14771  swrdccat3blem  14773  repswswrd  14818  repswpfx  14819  repswccat  14820  cshwidxmod  14837  2cshw  14847  3cshw  14852  scshwfzeqfzo  14861  cshwcsh2id  14863  cshimadifsn  14864  cshimadifsn0  14865  ccatco  14870  cshco  14871  swrdco  14872  pfxco  14873  lswco  14874  swrds2  14975  2swrd2eqwrdeq  14988  shftuz  15104  abs3dif  15366  fsumdifsnconst  15823  modfsummods  15825  sin02gt0  16224  dvdsval2  16289  dvdscmul  16316  dvdsmulc  16317  dvdscmulr  16318  dvdsmulcr  16319  divalglem8  16433  ndvdssub  16442  dvdsexpim  16588  rpmulgcd  16590  expgcd  16596  zexpgcd  16598  coprmprod  16694  cncongr1  16700  cncongr2  16701  isprm3  16716  modprm0  16838  coprimeprodsq  16841  pythagtriplem12  16859  pythagtriplem14  16861  pcprendvds  16873  pcmul  16884  pcdiv  16885  pcqcl  16889  pcqdiv  16890  pcdvdsb  16902  vdwnnlem1  17028  hashbcss  17037  cshwshashlem1  17129  fvsetsid  17201  setsstruct2  17207  setsstruct  17209  mrcss  17660  mrcsscl  17664  mrcun  17666  cofulid  17940  catcisolem  18163  funcsetcestrclem9  18218  latleeqj1  18508  lubun  18572  clatleglb  18575  pslem  18629  dirtr  18659  mgmb1mgm1  18680  pwspjmhm  18855  grpinvid1  19021  grpinvid2  19022  grpasscan1  19031  grpasscan2  19032  grpinvadd  19048  grpsubf  19049  grpsubrcan  19051  grpinvsub  19052  grpsubeq0  19056  grpsubadd0sub  19057  grppncan  19061  grpnpcan  19062  mulgnn0p1  19115  mulgaddcomlem  19127  mulginvcom  19129  mulginvinv  19130  subgsubcl  19167  subgsub  19168  eqglact  19209  qussub  19221  ghmsub  19254  psgnunilem4  19529  oddvds2  19598  odsubdvds  19603  gexnnod  19620  slwn0  19647  dvrcl  20420  unitdvcl  20421  dvrcan1  20425  dvrcan3  20426  dvreq1  20427  rngisom1  20482  rngisomring  20483  subrgdv  20605  abvsubtri  20844  idsrngd  20873  lmodvsubval2  20931  lsmcl  21099  lsmsp2  21103  lspsntrim  21114  rngqiprngimfolem  21317  lidldvgen  21361  cncrng  21418  chrcong  21559  dvdschrmulg  21560  zndvds  21585  zntoslem  21592  ocvsscon  21710  obselocv  21765  frlmphl  21818  ascldimul  21925  mpfsubrg  22144  ply1tmcl  22290  eqcoe1ply1eq  22318  gsummoncoe1  22327  lply1binomsc  22330  mamudm  22414  mamufacex  22415  scmatf1  22552  scmatf1o  22553  scmatrngiso  22557  submabas  22599  mdetdiaglem  22619  mdetralt2  22630  mdetero  22631  mdetunilem2  22634  mdetunilem6  22638  m2detleiblem7  22648  maducoeval2  22661  gsummatr01lem3  22678  gsummatr01  22680  smadiadetglem2  22693  cramerlem1  22708  mply1topmatcl  22826  mp2pm2mplem4  22830  ntrin  23084  elnei  23134  neindisj2  23146  ordtopn3  23219  leordtval2  23235  lecldbas  23242  cnrest2  23309  cmpsublem  23422  ptrescn  23662  xkococn  23683  kqfeq  23747  snfbas  23889  neifil  23903  fclsrest  24047  utopsnnei  24273  neipcfilu  24320  psmetsym  24335  psmetge0  24337  xmetge0  24369  xmetsym  24372  metustto  24581  metustbl  24594  restmetu  24598  nm2dif  24653  nmtri  24654  cnmet  24807  cnmpopc  24968  iihalf1  24971  iihalf2  24974  iocopnst  24983  clmnegsubdi2  25151  clmsub4  25152  clmvsubval2  25156  ncvspi  25203  cphsqrtcl3  25234  cph2ass  25260  cphipval2  25288  cphipval  25290  caublcls  25356  bcthlem3  25373  bcthlem4  25374  srabn  25407  cssbn  25422  cmslsschl  25424  rrxmet  25455  rrxdsfi  25458  iblconst  25867  dvdsq1p  26216  coeid3  26293  aannenlem2  26385  pserdvlem2  26486  tanord1  26593  cxpef  26721  recxpcl  26731  logbchbase  26828  relogbcl  26830  relogbzcl  26831  logbleb  26840  logblt  26841  relogbcxpb  26844  lawcos  26873  pythag  26874  isosctrlem1  26875  isosctrlem2  26876  lgsmodeq  27400  lgsmulsqcoprm  27401  gausslemma2dlem1a  27423  2lgsoddprmlem2  27467  sltres  27721  sletr  27817  cofcutr  27972  lrrecpo  27988  sltadd2im  28033  sleadd2im  28035  sleadd1  28036  sleadd2  28037  sltadd1  28039  addscan2  28040  addscan1  28041  sltsub1  28120  divsmulw  28232  ax5seglem1  28957  axcontlem2  28994  axcontlem8  29000  upgrpredgv  29170  numedglnl  29175  issubgr2  29303  uhgrissubgr  29306  egrsubgr  29308  nbusgrfi  29405  nb3grprlem2  29412  cplgr3v  29466  cusgrsizeindslem  29483  finsumvtxdg2size  29582  rusgrpropadjvtx  29617  upgrwlkvtxedg  29677  usgr2trlncl  29792  uspgrn2crct  29837  crctcshwlkn0lem4  29842  crctcshwlkn0lem5  29843  wwlksnextproplem3  29940  umgr2adedgwlklem  29973  rusgr0edg  30002  clwwlk1loop  30016  clwwlkccatlem  30017  clwlkclwwlklem2a4  30025  clwlkclwwlklem2a  30026  clwwisshclwwslemlem  30041  erclwwlktr  30050  clwwlkel  30074  erclwwlkntr  30099  clwwlknonex2lem2  30136  uhgr3cyclex  30210  umgr3cyclex  30211  eucrctshift  30271  frgr3v  30303  3cyclfrgrrn  30314  frgrwopreglem5a  30339  frgr2wsp1  30358  extwwlkfab  30380  clwwlknonclwlknonf1o  30390  numclwwlk3lem1  30410  numclwwlk5  30416  numclwwlk6  30418  isgrpo  30525  grpoinvid1  30556  grpoinvid2  30557  grpoinvop  30561  grpodivinv  30564  grpoinvdiv  30565  grpodivf  30566  grponpcan  30571  ablonncan  30584  nvmval  30670  nvmval2  30671  nvmfval  30672  nvmul0or  30678  nvpncan2  30681  nvaddsub4  30685  nvmeq0  30686  nvdif  30694  nvpi  30695  nvmtri  30699  nvabs  30700  imsmetlem  30718  ipval2lem3  30733  ipval2  30735  4ipval2  30736  ipval3  30737  nmooge0  30795  blometi  30831  hvaddsub12  31066  hvsubdistr1  31077  hvsubdistr2  31078  hvaddcan2  31099  hvmulcan  31100  hvmulcan2  31101  hvsubcan  31102  hvsubcan2  31103  his7  31118  his2sub  31120  his2sub2  31121  norm3dif2  31179  shsubcl  31248  hhssnv  31292  shlej2  31389  fh2  31647  cm2j  31648  pjoi0  31745  hodcl  31775  hosubdi  31836  unopf1o  31944  unopadj  31947  adj2  31962  braadd  31973  bramul  31974  lnopaddmuli  32001  lnopsubmuli  32003  homco2  32005  lnfnaddmuli  32073  adjlnop  32114  leopmul  32162  leoptr  32165  pjimai  32204  atcv1  32408  atexch  32409  atcvatlem  32413  fcoinvbr  32624  preiman0  32724  divnumden2  32821  xdivmul  32891  cshf1o  32931  resvsca  33335  idlsrgcmnd  33522  hasheuni  34065  difelsiga  34113  cndprobin  34415  bayesth  34420  sgn3da  34522  signstfvp  34564  breprexplemc  34625  fineqvac  35089  swrdrevpfx  35100  swrdwlk  35110  lediv2aALT  35661  fununiq  35749  dfrdg2  35776  clsun  36310  neiin  36314  rdgeqoa  37352  curfv  37586  matunitlindflem1  37602  poimirlem32  37638  ftc1anclem4  37682  areacirc  37699  filbcmb  37726  ismtybnd  37793  grpoeqdivid  37867  ghomco  37877  rngonegrmul  37930  zerdivemp1x  37933  rngohomco  37960  rngoisoco  37968  riscer  37974  intidl  38015  isfldidl  38054  brredunds  38607  lshpnelb  38965  opnlen0  39169  opcon3b  39177  opcon2b  39178  oplecon3b  39181  opltcon3b  39185  opltcon2b  39187  oldmm1  39198  oldmm4  39201  oldmj1  39202  oldmj4  39205  cvrval2  39255  cvrcon3b  39258  leatb  39273  atcmp  39292  atcvreq0  39295  atlatle  39301  athgt  39438  3dim2  39450  islln2a  39499  lplnnleat  39524  lvolnleat  39565  4atlem10  39588  4atlem11  39591  4atlem12  39594  dalem21  39676  dalem22  39677  dalem23  39678  dalem29  39683  dalem30  39684  dalem31N  39685  dalem32  39686  dalem33  39687  dalem34  39688  dalem35  39689  dalem36  39690  dalem37  39691  dalem40  39694  dalem46  39700  dalem47  39701  dalem51  39705  dalem52  39706  dalem58  39712  dalem59  39713  pmaple  39743  paddclN  39824  pmapjoin  39834  pmapjat1  39835  elpcliN  39875  pclssN  39876  pclun2N  39881  2polcon4bN  39900  paddunN  39909  poldmj1N  39910  pmapj2N  39911  pmapocjN  39912  psubclinN  39930  paddatclN  39931  poml4N  39935  lautco  40079  ldilco  40098  ltrneq2  40130  trljat1  40148  cdlemc1  40173  cdleme10  40236  ltrnco  40701  trlcocnv  40702  trljco  40722  trljco2  40723  cdlemi1  40800  tendocnv  41003  diaord  41029  dibord  41141  dihord3  41239  dihord4  41240  dihmeetlem2N  41281  dihmeetlem4preN  41288  dochdmj1  41372  hdmap10lem  41821  lcmineqlem1  42010  sticksstones2  42128  metakunt29  42214  metakunt30  42215  factwoffsmonot  42223  readdsub  42390  reltsub1  42392  renpncan3  42397  reppncan  42399  resubdi  42402  readdcan2  42418  mzprename  42736  dvdsrabdioph  42797  pell14qrdivcl  42852  monotoddzz  42931  jm2.19lem2  42978  jm2.19  42981  relexpaddss  43707  k0004lem3  44138  dvconstbi  44329  chordthmALT  44930  isosctrlem1ALT  44931  ssinc  45026  ssdec  45027  wessf1ornlem  45127  disjf1o  45133  ssnnf1octb  45136  projf1o  45139  mapssbi  45155  iunmapsn  45159  upbdrech  45255  iuneqfzuzlem  45283  suplesup  45288  rexabslelem  45367  climxrrelem  45704  limsupresxr  45721  liminfresxr  45722  liminfvalxr  45738  xlimliminflimsup  45817  cncfshift  45829  cncfperiod  45834  cncfuni  45841  icccncfext  45842  dvmptfprodlem  45899  dvnprodlem1  45901  itgspltprt  45934  ismbl3  45941  stoweidlem3  45958  stoweidlem10  45965  stoweidlem19  45974  stoweidlem31  45986  stoweidlem34  45989  stoweidlem44  45999  fourierdlem41  46103  fourierdlem42  46104  fourierdlem51  46112  fourierdlem68  46129  fourierdlem89  46150  fourierdlem91  46152  fourierdlem92  46153  fourierdlem94  46155  etransclem24  46213  etransclem34  46223  qndenserrnbllem  46249  salincl  46279  saldifcl2  46283  subsalsal  46314  sge0pr  46349  sge0pnffigt  46351  sge0reuz  46402  nnfoctbdjlem  46410  nnfoctbdj  46411  meadjiunlem  46420  caratheodorylem2  46482  hoidmv1le  46549  hoidmvlelem3  46552  hspmbllem2  46582  opnvonmbllem2  46588  sssmf  46693  smfaddlem1  46718  sigaraf  46808  sigarmf  46809  nltle2tri  47262  subsubelfzo0  47275  submodaddmod  47280  zplusmodne  47282  addmodne  47283  minusmod5ne  47288  submodneaddmod  47290  iccpartiltu  47346  icceuelpart  47360  poprelb  47448  reuopreuprim  47450  proththd  47538  mogoldbblem  47644  fppr2odd  47655  fpprel2  47665  bgoldbtbndlem2  47730  clnbusgrfi  47766  grimuhgr  47815  uhgrimisgrgric  47836  clnbgrgrim  47839  grtrif1o  47846  grlimgrtri  47898  gpgusgralem  47945  gpgedgvtx0  47953  gpg5nbgrvtx03starlem2  47959  nn0sumltlt  48194  invginvrid  48211  ply1sclrmsm  48228  linccl  48259  lincvalpr  48263  lincresunit3lem1  48324  lincresunit3  48326  fdivmpt  48389  nnolog2flm1  48439  dignnld  48452  digexp  48456  dignn0flhalflem1  48464  itcovalsucov  48517  reorelicc  48559  eenglngeehlnmlem1  48586  line2  48601  line2xlem  48602  itsclc0lem1  48605  itsclc0xyqsolr  48618  i0oii  48715  io1ii  48716  indthinc  48852  indthincALT  48853  setrec2fun  48922  reccot  48988  rectan  48989