Theorem 3adant2 1137

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  3ad2ant1  1139  3simpb  1155  3imp3i2an  1352  eupickb  2639  eqeu  3654  onunel  6424  iotan0  6482  funopg  6526  dff1o2  6779  fvelimad  6901  unima  6909  fnimapr  6917  fvmptt  6963  fnreseql  6996  xpprsng  7089  f1elima  7214  f1ounsn  7223  f13dfv  7225  f1ocnvfvb  7230  f1cdmsn  7233  f1ofvswap  7257  oprssov  7532  resf1extb  7881  resf1ext2b  7882  funelss  7996  poxp  8075  poxp2  8090  poxp3  8097  smoiso  8299  oaord  8479  oaword  8481  omcan  8501  omwordri  8504  odi  8511  omeulem1  8514  oeord  8521  oecan  8522  oewordri  8525  oeordsuc  8527  nnaord  8552  nnaordr  8553  nndi  8556  nnaword  8560  nnmwordri  8569  naddel2  8621  naddss1  8622  naddss2  8623  erov  8758  ecopovtrn  8764  mapsnd  8831  f1dom3g  8911  xpdom3  9010  mapxpen  9078  dif1en  9093  findcard  9095  f1domfi2  9113  entrfir  9122  domtrfil  9123  domtrfir  9125  sbthfilem  9129  sdomdomtrfi  9132  php3  9140  findcard3  9190  indexfi  9267  suppr  9382  infpr  9415  r111  9697  tcrank  9806  acndom  9971  infdif2  10129  infxpdom  10130  cfeq0  10176  cfsuc  10177  cfflb  10179  cflim2  10183  cfsmolem  10190  axcc3  10358  domtriomlem  10362  axdc3lem2  10371  axdc3lem4  10373  axdc4lem  10375  axcclem  10377  pwcfsdom  10504  tsktrss  10682  tsksuc  10683  tskuni  10704  adderpqlem  10875  mulerpqlem  10876  mulcanenq  10881  distrnq  10882  ltsonq  10890  ltanq  10892  ltmnq  10893  distrlem1pr  10946  distrlem5pr  10948  ltsopr  10953  ltsosr  11015  ltasr  11021  adddir  11133  axlttrn  11216  letr  11238  nnncan1  11428  npncan3  11430  pnpcan2  11432  subdi  11581  subdir  11582  mulcan1g  11801  mulcan2g  11802  divmul  11810  div23  11826  div13  11828  muldivdir  11845  divsubdir  11846  subdivcomb1  11848  divcan7  11862  ltmul2  12004  lemul1  12005  lemul2  12006  lemul2a  12008  lediv1  12019  ltmuldiv2  12028  lemuldiv  12034  lemuldiv2  12035  ltdiv2  12040  lediv2  12044  infrelb  12139  nndivtr  12222  bndndx  12434  nn0n0n1ge2  12503  fnn0ind  12626  addlelt  13056  xrletr  13107  qsqueeze  13151  xleadd2a  13204  xleadd1  13205  xltadd2  13207  xltmul2  13243  supxrbnd  13278  iooneg  13422  iccneg  13423  icoshft  13424  icoshftf1o  13425  zltaddlt1le  13456  fzen  13493  uzsubsubfz  13498  ssfzunsnext  13521  fzrevral2  13565  fzshftral  13567  fz0fzdiffz0  13589  elfzmlbp  13591  elfzo  13613  nelfzo  13617  fzoaddel2  13673  fzosubel2  13678  ssfzo12bi  13714  fzonfzoufzol  13724  subfzo0  13745  flltdivnn0lt  13790  modmulnn  13846  modcyc  13863  modaddabs  13868  modaddmod  13869  modmuladd  13873  modadd2mod  13881  modsubmod  13889  modsubmodmod  13890  modaddmodup  13894  modmulmod  13896  modsubdir  13900  modfzo0difsn  13903  modsumfzodifsn  13904  uzindi  13942  axdc4uzlem  13943  expneg2  14030  expdiv  14073  expubnd  14138  mulbinom2  14183  bernneq2  14190  expnngt1  14201  hashinfxadd  14345  hashunsngx  14353  hashunsnggt  14354  hashfundm  14402  hashf1dmcdm  14404  hashdifsnp1  14466  ccatval3  14539  ccatfv0  14544  ccatval1lsw  14545  ccats1val2  14588  ccatw2s1p1  14597  swrdnd  14615  pfxsuffeqwrdeq  14658  pfxsuff1eqwrdeq  14659  swrdswrd  14665  pfxpfx  14668  wrd2ind  14683  swrdccatin1  14685  pfxccatin12lem1  14688  swrdccatin2  14689  pfxccatin12lem3  14692  swrdccat  14695  pfxccatpfx1  14696  pfxccatpfx2  14697  swrdccat3blem  14699  repswswrd  14744  repswpfx  14745  repswccat  14746  cshwidxmod  14763  2cshw  14773  3cshw  14778  scshwfzeqfzo  14786  cshwcsh2id  14788  cshimadifsn  14789  cshimadifsn0  14790  ccatco  14795  cshco  14796  swrdco  14797  pfxco  14798  lswco  14799  swrds2  14900  2swrd2eqwrdeq  14913  shftuz  15029  abs3dif  15292  fsumdifsnconst  15752  modfsummods  15754  sin02gt0  16157  dvdsval2  16222  dvdscmul  16249  dvdsmulc  16250  dvdscmulr  16251  dvdsmulcr  16252  divalglem8  16367  ndvdssub  16376  dvdsexpim  16522  rpmulgcd  16524  expgcd  16530  zexpgcd  16532  coprmprod  16628  cncongr1  16634  cncongr2  16635  isprm3  16650  modprm0  16774  coprimeprodsq  16777  pythagtriplem12  16795  pythagtriplem14  16797  pcprendvds  16809  pcmul  16820  pcdiv  16821  pcqcl  16825  pcqdiv  16826  pcdvdsb  16838  vdwnnlem1  16964  hashbcss  16973  cshwshashlem1  17064  fvsetsid  17136  setsstruct2  17142  setsstruct  17144  mrcss  17580  mrcsscl  17584  mrcun  17586  cofulid  17855  catcisolem  18075  funcsetcestrclem9  18127  latleeqj1  18415  lubun  18479  clatleglb  18482  pslem  18536  dirtr  18566  mgmb1mgm1  18621  pwspjmhm  18796  grpinvid1  18965  grpinvid2  18966  grpasscan1  18975  grpasscan2  18976  grpinvadd  18992  grpsubf  18993  grpsubrcan  18995  grpinvsub  18996  grpsubeq0  19000  grpsubadd0sub  19001  grppncan  19005  grpnpcan  19006  mulgnn0p1  19059  mulgaddcomlem  19071  mulginvcom  19073  mulginvinv  19074  subgsubcl  19111  subgsub  19112  eqglact  19152  qussub  19164  ghmsub  19197  psgnunilem4  19470  oddvds2  19539  odsubdvds  19544  gexnnod  19561  slwn0  19588  dvrcl  20382  unitdvcl  20383  dvrcan1  20387  dvrcan3  20388  dvreq1  20389  rngisom1  20444  rngisomring  20445  subrgdv  20568  abvsubtri  20806  idsrngd  20835  lmodvsubval2  20914  lsmcl  21080  lsmsp2  21084  lspsntrim  21095  rngqiprngimfolem  21290  lidldvgen  21334  cncrng  21375  chrcong  21509  dvdschrmulg  21510  zndvds  21531  zntoslem  21538  ocvsscon  21657  obselocv  21710  frlmphl  21763  ascldimul  21870  mpfsubrg  22094  ply1tmcl  22265  eqcoe1ply1eq  22292  gsummoncoe1  22301  lply1binomsc  22304  mamudm  22385  mamufacex  22386  scmatf1  22521  scmatf1o  22522  scmatrngiso  22526  submabas  22568  mdetdiaglem  22588  mdetralt2  22599  mdetero  22600  mdetunilem2  22603  mdetunilem6  22607  m2detleiblem7  22617  maducoeval2  22630  gsummatr01lem3  22647  gsummatr01  22649  smadiadetglem2  22662  cramerlem1  22677  mply1topmatcl  22795  mp2pm2mplem4  22799  ntrin  23051  elnei  23101  neindisj2  23113  ordtopn3  23186  leordtval2  23202  lecldbas  23209  cnrest2  23276  cmpsublem  23389  ptrescn  23629  xkococn  23650  kqfeq  23714  snfbas  23856  neifil  23870  fclsrest  24014  utopsnnei  24239  neipcfilu  24285  psmetsym  24300  psmetge0  24302  xmetge0  24334  xmetsym  24337  metustto  24543  metustbl  24556  restmetu  24560  nm2dif  24615  nmtri  24616  cnmet  24761  cnmpopc  24920  iihalf1  24923  iihalf2  24925  iocopnst  24932  clmnegsubdi2  25097  clmsub4  25098  clmvsubval2  25102  ncvspi  25148  cphsqrtcl3  25179  cph2ass  25205  cphipval2  25233  cphipval  25235  caublcls  25301  bcthlem3  25318  bcthlem4  25319  srabn  25352  cssbn  25367  cmslsschl  25369  rrxmet  25400  rrxdsfi  25403  iblconst  25810  dvdsq1p  26153  coeid3  26230  aannenlem2  26320  pserdvlem2  26418  tanord1  26526  cxpef  26654  recxpcl  26664  logbchbase  26760  relogbcl  26762  relogbzcl  26763  logbleb  26772  logblt  26773  relogbcxpb  26776  lawcos  26805  pythag  26806  isosctrlem1  26807  isosctrlem2  26808  lgsmodeq  27330  lgsmulsqcoprm  27331  gausslemma2dlem1a  27353  2lgsoddprmlem2  27397  ltsres  27651  lestr  27751  cofcutr  27941  lrrecpo  27958  ltadds2im  28003  leadds2im  28005  leadds1  28006  leadds2  28007  ltadds1  28009  addscan2  28010  addscan1  28011  ltsubs1  28093  divmulsw  28210  oldfib  28394  zsoring  28426  bdayfinbndlem1  28484  ax5seglem1  29022  axcontlem2  29059  axcontlem8  29065  upgrpredgv  29233  numedglnl  29238  issubgr2  29366  uhgrissubgr  29369  egrsubgr  29371  nbusgrfi  29468  nb3grprlem2  29475  cplgr3v  29529  cusgrsizeindslem  29545  finsumvtxdg2size  29644  rusgrpropadjvtx  29679  upgrwlkvtxedg  29738  usgr2trlncl  29853  uspgrn2crct  29901  crctcshwlkn0lem4  29906  crctcshwlkn0lem5  29907  wwlksnextproplem3  30004  umgr2adedgwlklem  30037  rusgr0edg  30069  clwwlk1loop  30083  clwwlkccatlem  30084  clwlkclwwlklem2a4  30092  clwlkclwwlklem2a  30093  clwwisshclwwslemlem  30108  erclwwlktr  30117  clwwlkel  30141  erclwwlkntr  30166  clwwlknonex2lem2  30203  uhgr3cyclex  30277  umgr3cyclex  30278  eucrctshift  30338  frgr3v  30370  3cyclfrgrrn  30381  frgrwopreglem5a  30406  frgr2wsp1  30425  extwwlkfab  30447  clwwlknonclwlknonf1o  30457  numclwwlk3lem1  30477  numclwwlk5  30483  numclwwlk6  30485  isgrpo  30593  grpoinvid1  30624  grpoinvid2  30625  grpoinvop  30629  grpodivinv  30632  grpoinvdiv  30633  grpodivf  30634  grponpcan  30639  ablonncan  30652  nvmval  30738  nvmval2  30739  nvmfval  30740  nvmul0or  30746  nvpncan2  30749  nvaddsub4  30753  nvmeq0  30754  nvdif  30762  nvpi  30763  nvmtri  30767  nvabs  30768  imsmetlem  30786  ipval2lem3  30801  ipval2  30803  4ipval2  30804  ipval3  30805  nmooge0  30863  blometi  30899  hvaddsub12  31134  hvsubdistr1  31145  hvsubdistr2  31146  hvaddcan2  31167  hvmulcan  31168  hvmulcan2  31169  hvsubcan  31170  hvsubcan2  31171  his7  31186  his2sub  31188  his2sub2  31189  norm3dif2  31247  shsubcl  31316  hhssnv  31360  shlej2  31457  fh2  31715  cm2j  31716  pjoi0  31813  hodcl  31843  hosubdi  31904  unopf1o  32012  unopadj  32015  adj2  32030  braadd  32041  bramul  32042  lnopaddmuli  32069  lnopsubmuli  32071  homco2  32073  lnfnaddmuli  32141  adjlnop  32182  leopmul  32230  leoptr  32233  pjimai  32272  atcv1  32476  atexch  32477  atcvatlem  32481  fcoinvbr  32701  preiman0  32809  divnumden2  32915  sgn3da  32933  xdivmul  33010  cshf1o  33048  resvsca  33422  idlsrgcmnd  33605  hasheuni  34276  difelsiga  34324  cndprobin  34625  bayesth  34630  signstfvp  34762  breprexplemc  34823  trssfir1om  35299  fineqvac  35304  fineqvnttrclselem1  35309  fineqvnttrclselem3  35311  trssfir1omregs  35324  swrdrevpfx  35352  swrdwlk  35362  lediv2aALT  35912  fununiq  36004  dfrdg2  36028  clsun  36563  neiin  36567  rdgeqoa  37739  curfv  37974  matunitlindflem1  37990  poimirlem32  38026  ftc1anclem4  38070  areacirc  38087  filbcmb  38114  ismtybnd  38181  grpoeqdivid  38255  ghomco  38265  rngonegrmul  38318  zerdivemp1x  38321  rngohomco  38348  rngoisoco  38356  riscer  38362  intidl  38403  isfldidl  38442  eceldmqsxrncnvepres  38810  eceldmqsxrncnvepres2  38811  brredunds  39084  lshpnelb  39483  opnlen0  39687  opcon3b  39695  opcon2b  39696  oplecon3b  39699  opltcon3b  39703  opltcon2b  39705  oldmm1  39716  oldmm4  39719  oldmj1  39720  oldmj4  39723  cvrval2  39773  cvrcon3b  39776  leatb  39791  atcmp  39810  atcvreq0  39813  atlatle  39819  athgt  39955  3dim2  39967  islln2a  40016  lplnnleat  40041  lvolnleat  40082  4atlem10  40105  4atlem11  40108  4atlem12  40111  dalem21  40193  dalem22  40194  dalem23  40195  dalem29  40200  dalem30  40201  dalem31N  40202  dalem32  40203  dalem33  40204  dalem34  40205  dalem35  40206  dalem36  40207  dalem37  40208  dalem40  40211  dalem46  40217  dalem47  40218  dalem51  40222  dalem52  40223  dalem58  40229  dalem59  40230  pmaple  40260  paddclN  40341  pmapjoin  40351  pmapjat1  40352  elpcliN  40392  pclssN  40393  pclun2N  40398  2polcon4bN  40417  paddunN  40426  poldmj1N  40427  pmapj2N  40428  pmapocjN  40429  psubclinN  40447  paddatclN  40448  poml4N  40452  lautco  40596  ldilco  40615  ltrneq2  40647  trljat1  40665  cdlemc1  40690  cdleme10  40753  ltrnco  41218  trlcocnv  41219  trljco  41239  trljco2  41240  cdlemi1  41317  tendocnv  41520  diaord  41546  dibord  41658  dihord3  41756  dihord4  41757  dihmeetlem2N  41798  dihmeetlem4preN  41805  dochdmj1  41889  hdmap10lem  42338  lcmineqlem1  42521  sticksstones2  42639  readdsub  42868  reltsub1  42870  renpncan3  42875  reppncan  42877  resubdi  42880  readdcan2  42897  mzprename  43205  dvdsrabdioph  43262  pell14qrdivcl  43317  monotoddzz  43395  jm2.19lem2  43442  jm2.19  43445  relexpaddss  44169  k0004lem3  44600  dvconstbi  44785  chordthmALT  45383  isosctrlem1ALT  45384  ssinc  45541  ssdec  45542  wessf1ornlem  45639  disjf1o  45645  ssnnf1octb  45648  projf1o  45650  mapssbi  45665  iunmapsn  45669  upbdrech  45760  iuneqfzuzlem  45786  suplesup  45791  rexabslelem  45868  climxrrelem  46199  limsupresxr  46216  liminfresxr  46217  liminfvalxr  46233  xlimliminflimsup  46312  cncfshift  46324  cncfperiod  46329  cncfuni  46336  icccncfext  46337  dvmptfprodlem  46394  dvnprodlem1  46396  itgspltprt  46429  ismbl3  46436  stoweidlem3  46453  stoweidlem10  46460  stoweidlem19  46469  stoweidlem31  46481  stoweidlem34  46484  stoweidlem44  46494  fourierdlem41  46598  fourierdlem42  46599  fourierdlem51  46607  fourierdlem68  46624  fourierdlem89  46645  fourierdlem91  46647  fourierdlem92  46648  fourierdlem94  46650  etransclem24  46708  etransclem34  46718  qndenserrnbllem  46744  salincl  46774  saldifcl2  46778  subsalsal  46809  sge0pr  46844  sge0pnffigt  46846  sge0reuz  46897  nnfoctbdjlem  46905  nnfoctbdj  46906  meadjiunlem  46915  caratheodorylem2  46977  hoidmv1le  47044  hoidmvlelem3  47047  hspmbllem2  47077  opnvonmbllem2  47083  sssmf  47188  smfaddlem1  47213  sigaraf  47303  sigarmf  47304  nltle2tri  47783  subsubelfzo0  47797  nnmul2  47800  submodaddmod  47817  zplusmodne  47819  addmodne  47820  minusmod5ne  47825  submodneaddmod  47827  modmkpkne  47837  modmknepk  47838  iccpartiltu  47904  icceuelpart  47918  poprelb  48006  reuopreuprim  48008  nprmmul2  48010  proththd  48099  mogoldbblem  48218  fppr2odd  48229  fpprel2  48239  bgoldbtbndlem2  48304  clnbusgrfi  48341  grimuhgr  48385  uhgrimisgrgric  48429  clnbgrgrim  48432  grtrif1o  48440  grlimgrtri  48501  gpgusgralem  48554  gpgedgvtx0  48559  gpgedg2ov  48564  gpgedg2iv  48565  gpg5nbgrvtx03starlem2  48567  nn0sumltlt  48848  invginvrid  48865  ply1sclrmsm  48882  linccl  48912  lincvalpr  48916  lincresunit3lem1  48977  lincresunit3  48979  fdivmpt  49038  nnolog2flm1  49088  dignnld  49101  digexp  49105  dignn0flhalflem1  49113  itcovalsucov  49166  reorelicc  49208  eenglngeehlnmlem1  49235  line2  49250  line2xlem  49251  itsclc0lem1  49254  itsclc0xyqsolr  49267  i0oii  49417  io1ii  49418  indthinc  49959  indthincALT  49960  setrec2fun  50189  reccot  50255  rectan  50256