Theorem 3adant2 1127

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  3ad2ant1  1129  3simpb  1145  3imp3i2an  1341  eupickb  2716  vtoclegft  3581  eqeu  3696  iotan0  6344  funopg  6388  fnco  6464  dff1o2  6619  fvelimad  6731  unima  6738  fnimapr  6746  fvmptt  6787  fnreseql  6817  xpprsng  6901  f1elima  7020  f13dfv  7030  f1ocnvfvb  7035  oprssov  7316  funelss  7745  poxp  7821  wfrlem4  7957  smoiso  7998  oaord  8172  oaword  8174  omcan  8194  omwordri  8197  odi  8204  omeulem1  8207  oeord  8213  oecan  8214  oewordri  8217  oeordsuc  8219  nnaord  8244  nnaordr  8245  nndi  8248  nnaword  8252  nnmwordri  8261  erov  8393  ecopovtrn  8399  mapsnd  8449  xpdom3  8614  mapxpen  8682  findcard  8756  indexfi  8831  suppr  8934  infpr  8966  r111  9203  tcrank  9312  acndom  9476  infdif2  9631  infxpdom  9632  cfeq0  9677  cfsuc  9678  cfflb  9680  cflim2  9684  cfsmolem  9691  axcc3  9859  domtriomlem  9863  axdc3lem2  9872  axdc3lem4  9874  axdc4lem  9876  axcclem  9878  pwcfsdom  10004  tsktrss  10182  tsksuc  10183  tskuni  10204  adderpqlem  10375  mulerpqlem  10376  mulcanenq  10381  distrnq  10382  ltsonq  10390  ltanq  10392  ltmnq  10393  distrlem1pr  10446  distrlem5pr  10448  ltsopr  10453  ltsosr  10515  ltasr  10521  adddir  10631  axlttrn  10712  letr  10733  nnncan1  10921  npncan3  10923  pnpcan2  10925  subdi  11072  subdir  11073  mulcan1g  11292  mulcan2g  11293  divmul  11300  div23  11316  div13  11318  muldivdir  11332  divsubdir  11333  subdivcomb1  11334  divcan7  11348  ltmul2  11490  lemul1  11491  lemul2  11492  lemul2a  11494  lediv1  11504  ltmuldiv2  11513  lemuldiv  11519  lemuldiv2  11520  ltdiv2  11525  lediv2  11529  fiminreOLD  11589  infrelb  11625  nndivtr  11683  bndndx  11895  nn0n0n1ge2  11961  fnn0ind  12080  addlelt  12502  xrletr  12550  qsqueeze  12593  xleadd2a  12646  xleadd1  12647  xltadd2  12649  xltmul2  12685  supxrbnd  12720  iooneg  12856  iccneg  12857  icoshft  12858  icoshftf1o  12859  zltaddlt1le  12889  fzen  12923  uzsubsubfz  12928  ssfzunsnext  12951  fzrevral2  12992  fzshftral  12994  fz0fzdiffz0  13015  elfzmlbp  13017  elfzo  13039  nelfzo  13042  fzoaddel2  13092  fzosubel2  13096  ssfzo12bi  13131  fzonfzoufzol  13139  subfzo0  13158  flltdivnn0lt  13202  modmulnn  13256  modcyc  13273  modaddabs  13276  modaddmod  13277  modmuladd  13280  modadd2mod  13288  modsubmod  13296  modsubmodmod  13297  modaddmodup  13301  modmulmod  13303  modsubdir  13307  modfzo0difsn  13310  modsumfzodifsn  13311  uzindi  13349  axdc4uzlem  13350  expneg2  13437  expdiv  13479  expubnd  13540  mulbinom2  13583  bernneq2  13590  expnngt1  13601  hashinfxadd  13745  hashunsngx  13753  hashunsnggt  13754  hashdifsnp1  13853  ccatval3  13932  ccatfv0  13936  ccatval1lsw  13937  ccats1val2  13982  ccatw2s1p1  13994  swrdnd  14015  pfxsuffeqwrdeq  14059  pfxsuff1eqwrdeq  14060  swrdswrd  14066  pfxpfx  14069  wrd2ind  14084  swrdccatin1  14086  pfxccatin12lem1  14089  swrdccatin2  14090  pfxccatin12lem3  14093  swrdccat  14096  pfxccatpfx1  14097  pfxccatpfx2  14098  swrdccat3blem  14100  repswswrd  14145  repswpfx  14146  repswccat  14147  cshwidxmod  14164  2cshw  14174  3cshw  14179  scshwfzeqfzo  14187  cshwcsh2id  14189  cshimadifsn  14190  cshimadifsn0  14191  ccatco  14196  cshco  14197  swrdco  14198  pfxco  14199  lswco  14200  swrds2  14301  2swrd2eqwrdeq  14314  shftuz  14427  abs3dif  14690  fsumdifsnconst  15145  modfsummods  15147  sin02gt0  15544  dvdsval2  15609  dvdscmul  15635  dvdsmulc  15636  dvdscmulr  15637  dvdsmulcr  15638  divalglem8  15750  ndvdssub  15759  rpmulgcd  15905  coprmprod  16004  cncongr1  16010  cncongr2  16011  isprm3  16026  modprm0  16141  coprimeprodsq  16144  pythagtriplem12  16162  pythagtriplem14  16164  pcprendvds  16176  pcmul  16187  pcdiv  16188  pcqcl  16192  pcqdiv  16193  pcdvdsb  16204  vdwnnlem1  16330  hashbcss  16339  cshwshashlem1  16428  fvsetsid  16514  setsstruct2  16520  setsstruct  16522  mrcss  16886  mrcsscl  16890  mrcun  16892  cofulid  17159  catcisolem  17365  funcsetcestrclem9  17412  latleeqj1  17672  lubun  17732  clatleglb  17735  pslem  17815  dirtr  17845  mgmb1mgm1  17864  pwspjmhm  17993  grpinvid1  18153  grpinvid2  18154  grpasscan1  18161  grpasscan2  18162  grpinvadd  18176  grpsubf  18177  grpsubrcan  18179  grpinvsub  18180  grpsubeq0  18184  grpsubadd0sub  18185  grppncan  18189  grpnpcan  18190  mulgnn0p1  18238  mulgaddcomlem  18249  mulginvcom  18251  mulginvinv  18252  subgsubcl  18289  subgsub  18290  eqglact  18330  qussub  18339  ghmsub  18365  psgnunilem4  18624  oddvds2  18692  odsubdvds  18695  gexnnod  18712  slwn0  18739  dvrcl  19435  unitdvcl  19436  dvrcan1  19440  dvrcan3  19441  dvreq1  19442  subrgdv  19551  abvsubtri  19605  idsrngd  19632  lmodvsubval2  19688  lsmcl  19854  lsmsp2  19858  lspsntrim  19869  lidldvgen  20027  ascldimul  20115  mpfsubrg  20315  ply1tmcl  20439  eqcoe1ply1eq  20464  gsummoncoe1  20471  lply1binomsc  20474  chrcong  20675  zndvds  20695  zntoslem  20702  ocvsscon  20818  obselocv  20871  frlmphl  20924  mamudm  20998  mamufacex  20999  scmatf1  21139  scmatf1o  21140  scmatrngiso  21144  submabas  21186  mdetdiaglem  21206  mdetralt2  21217  mdetero  21218  mdetunilem2  21221  mdetunilem6  21225  m2detleiblem7  21235  maducoeval2  21248  gsummatr01lem3  21265  gsummatr01  21267  smadiadetglem2  21280  cramerlem1  21295  mply1topmatcl  21412  mp2pm2mplem4  21416  ntrin  21668  elnei  21718  neindisj2  21730  ordtopn3  21803  leordtval2  21819  lecldbas  21826  cnrest2  21893  cmpsublem  22006  ptrescn  22246  xkococn  22267  kqfeq  22331  snfbas  22473  neifil  22487  fclsrest  22631  utopsnnei  22857  neipcfilu  22904  psmetsym  22919  psmetge0  22921  xmetge0  22953  xmetsym  22956  metustto  23162  metustbl  23175  restmetu  23179  nm2dif  23233  nmtri  23234  cnmet  23379  cnmpopc  23531  iihalf1  23534  iihalf2  23536  iocopnst  23543  clmnegsubdi2  23708  clmsub4  23709  clmvsubval2  23713  ncvspi  23759  cphsqrtcl3  23790  cph2ass  23816  cphipval2  23843  cphipval  23845  caublcls  23911  bcthlem3  23928  bcthlem4  23929  srabn  23962  cssbn  23977  cmslsschl  23979  rrxmet  24010  rrxdsfi  24013  iblconst  24417  tdeglem3  24652  mdegmullem  24671  dvdsq1p  24753  coeid3  24829  aannenlem2  24917  pserdvlem2  25015  tanord1  25120  cxpef  25247  recxpcl  25257  logbchbase  25348  relogbcl  25350  relogbzcl  25351  logbleb  25360  logblt  25361  relogbcxpb  25364  lawcos  25393  pythag  25394  isosctrlem1  25395  isosctrlem2  25396  lgsmodeq  25917  lgsmulsqcoprm  25918  gausslemma2dlem1a  25940  2lgsoddprmlem2  25984  ax5seglem1  26713  axcontlem2  26750  axcontlem8  26756  upgrpredgv  26923  numedglnl  26928  issubgr2  27053  uhgrissubgr  27056  egrsubgr  27058  nbusgrfi  27155  nb3grprlem2  27162  cplgr3v  27216  cusgrsizeindslem  27232  finsumvtxdg2size  27331  rusgrpropadjvtx  27366  upgrwlkvtxedg  27425  usgr2trlncl  27540  uspgrn2crct  27585  crctcshwlkn0lem4  27590  crctcshwlkn0lem5  27591  wwlksnextproplem3  27689  umgr2adedgwlklem  27722  rusgr0edg  27751  clwwlk1loop  27765  clwwlkccatlem  27766  clwlkclwwlklem2a4  27774  clwlkclwwlklem2a  27775  clwwisshclwwslemlem  27790  erclwwlktr  27799  clwwlkel  27824  erclwwlkntr  27849  clwwlknonex2lem2  27886  uhgr3cyclex  27960  umgr3cyclex  27961  eucrctshift  28021  frgr3v  28053  3cyclfrgrrn  28064  frgrwopreglem5a  28089  frgr2wsp1  28108  extwwlkfab  28130  clwwlknonclwlknonf1o  28140  numclwwlk3lem1  28160  numclwwlk5  28166  numclwwlk6  28168  isgrpo  28273  grpoinvid1  28304  grpoinvid2  28305  grpoinvop  28309  grpodivinv  28312  grpoinvdiv  28313  grpodivf  28314  grponpcan  28319  ablonncan  28332  nvmval  28418  nvmval2  28419  nvmfval  28420  nvmul0or  28426  nvpncan2  28429  nvaddsub4  28433  nvmeq0  28434  nvdif  28442  nvpi  28443  nvmtri  28447  nvabs  28448  imsmetlem  28466  ipval2lem3  28481  ipval2  28483  4ipval2  28484  ipval3  28485  nmooge0  28543  blometi  28579  hvaddsub12  28814  hvsubdistr1  28825  hvsubdistr2  28826  hvaddcan2  28847  hvmulcan  28848  hvmulcan2  28849  hvsubcan  28850  hvsubcan2  28851  his7  28866  his2sub  28868  his2sub2  28869  norm3dif2  28927  shsubcl  28996  hhssnv  29040  shlej2  29137  fh2  29395  cm2j  29396  pjoi0  29493  hodcl  29523  hosubdi  29584  unopf1o  29692  unopadj  29695  adj2  29710  braadd  29721  bramul  29722  lnopaddmuli  29749  lnopsubmuli  29751  homco2  29753  lnfnaddmuli  29821  adjlnop  29862  leopmul  29910  leoptr  29913  pjimai  29952  atcv1  30156  atexch  30157  atcvatlem  30161  fcoinvbr  30357  divnumden2  30533  xdivmul  30601  cshf1o  30636  dvdschrmulg  30858  resvsca  30903  hasheuni  31344  difelsiga  31392  cndprobin  31692  bayesth  31697  sgn3da  31799  signstfvp  31841  breprexplemc  31903  hashfundm  32354  hashf1dmcdm  32356  swrdrevpfx  32363  swrdwlk  32373  lediv2aALT  32920  fununiq  33012  dfrdg2  33040  sltres  33169  sletr  33237  clsun  33676  neiin  33680  rdgeqoa  34650  curfv  34871  matunitlindflem1  34887  poimirlem32  34923  ftc1anclem4  34969  areacirc  34986  filbcmb  35014  ismtybnd  35084  grpoeqdivid  35158  ghomco  35168  rngonegrmul  35221  zerdivemp1x  35224  rngohomco  35251  rngoisoco  35259  riscer  35265  intidl  35306  isfldidl  35345  brredunds  35860  lshpnelb  36119  opnlen0  36323  opcon3b  36331  opcon2b  36332  oplecon3b  36335  opltcon3b  36339  opltcon2b  36341  oldmm1  36352  oldmm4  36355  oldmj1  36356  oldmj4  36359  cvrval2  36409  cvrcon3b  36412  leatb  36427  atcmp  36446  atcvreq0  36449  atlatle  36455  athgt  36591  3dim2  36603  islln2a  36652  lplnnleat  36677  lvolnleat  36718  4atlem10  36741  4atlem11  36744  4atlem12  36747  dalem21  36829  dalem22  36830  dalem23  36831  dalem29  36836  dalem30  36837  dalem31N  36838  dalem32  36839  dalem33  36840  dalem34  36841  dalem35  36842  dalem36  36843  dalem37  36844  dalem40  36847  dalem46  36853  dalem47  36854  dalem51  36858  dalem52  36859  dalem58  36865  dalem59  36866  pmaple  36896  paddclN  36977  pmapjoin  36987  pmapjat1  36988  elpcliN  37028  pclssN  37029  pclun2N  37034  2polcon4bN  37053  paddunN  37062  poldmj1N  37063  pmapj2N  37064  pmapocjN  37065  psubclinN  37083  paddatclN  37084  poml4N  37088  lautco  37232  ldilco  37251  ltrneq2  37283  trljat1  37301  cdlemc1  37326  cdleme10  37389  ltrnco  37854  trlcocnv  37855  trljco  37875  trljco2  37876  cdlemi1  37953  tendocnv  38156  diaord  38182  dibord  38294  dihord3  38392  dihord4  38393  dihmeetlem2N  38434  dihmeetlem4preN  38441  dochdmj1  38525  hdmap10lem  38974  dvdsexpim  39179  expgcd  39181  zexpgcd  39183  readdsub  39212  reltsub1  39214  renpncan3  39219  reppncan  39221  resubdi  39224  readdcan2  39240  mzprename  39344  dvdsrabdioph  39405  pell14qrdivcl  39460  monotoddzz  39538  jm2.19lem2  39585  jm2.19  39588  relexpaddss  40061  k0004lem3  40497  dvconstbi  40664  chordthmALT  41265  isosctrlem1ALT  41266  ssinc  41351  ssdec  41352  wessf1ornlem  41443  disjf1o  41450  disjinfi  41452  ssnnf1octb  41454  projf1o  41457  mapssbi  41474  iunmapsn  41478  upbdrech  41570  iuneqfzuzlem  41600  suplesup  41605  rexabslelem  41690  climxrrelem  42028  limsupresxr  42045  liminfresxr  42046  liminfvalxr  42062  xlimliminflimsup  42141  cncfshift  42155  cncfperiod  42160  cncfuni  42167  icccncfext  42168  dvmptfprodlem  42227  dvnprodlem1  42229  itgspltprt  42262  ismbl3  42270  stoweidlem3  42287  stoweidlem10  42294  stoweidlem19  42303  stoweidlem31  42315  stoweidlem34  42318  stoweidlem44  42328  fourierdlem41  42432  fourierdlem42  42433  fourierdlem51  42441  fourierdlem68  42458  fourierdlem89  42479  fourierdlem91  42481  fourierdlem92  42482  fourierdlem94  42484  etransclem24  42542  etransclem34  42552  qndenserrnbllem  42578  salincl  42607  saldifcl2  42610  subsalsal  42641  sge0pr  42675  sge0pnffigt  42677  sge0reuz  42728  nnfoctbdjlem  42736  nnfoctbdj  42737  meadjiunlem  42746  caratheodorylem2  42808  hoidmv1le  42875  hoidmvlelem3  42878  hspmbllem2  42908  opnvonmbllem2  42914  sssmf  43014  smfaddlem1  43038  sigaraf  43109  sigarmf  43110  nltle2tri  43512  subsubelfzo0  43525  iccpartiltu  43581  icceuelpart  43595  poprelb  43685  reuopreuprim  43687  proththd  43778  mogoldbblem  43884  fppr2odd  43895  fpprel2  43905  bgoldbtbndlem2  43970  isomgrtr  44003  nn0sumltlt  44397  invginvrid  44414  ply1sclrmsm  44436  linccl  44468  lincvalpr  44472  lincresunit3lem1  44533  lincresunit3  44535  fdivmpt  44599  nnolog2flm1  44649  dignnld  44662  digexp  44666  dignn0flhalflem1  44674  reorelicc  44696  eenglngeehlnmlem1  44723  line2  44738  line2xlem  44739  itsclc0lem1  44742  itsclc0xyqsolr  44755  setrec2fun  44794  reccot  44856  rectan  44857