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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  3ad2ant1  1151  3simpb  1167  3imp3i2an  1364  eupickb  2663  eqeu  3670  onunel  6470  iotan0  6528  funopg  6572  dff1o2  6828  fvelimad  6950  unima  6958  fnimapr  6966  fvmptt  7012  fnreseql  7045  xpprsng  7138  f1elima  7263  f1ounsn  7272  f13dfv  7274  f1ocnvfvb  7279  f1cdmsn  7282  f1ofvswap  7306  oprssov  7581  resf1extb  7932  resf1ext2b  7933  funelss  8045  poxp  8125  poxp2  8140  poxp3  8147  smoiso  8350  oaord  8533  oaword  8535  omcan  8555  omwordri  8558  odi  8565  omeulem1  8568  oeord  8575  oecan  8576  oewordri  8579  oeordsuc  8581  nnaord  8606  nnaordr  8607  nndi  8610  nnaword  8614  nnmwordri  8623  naddel2  8676  naddss1  8677  naddss2  8678  erov  8813  ecopovtrn  8819  mapsnd  8885  f1dom3g  8965  xpdom3  9064  mapxpen  9132  dif1en  9147  findcard  9149  f1domfi2  9167  entrfir  9176  domtrfil  9177  domtrfir  9179  sbthfilem  9183  sdomdomtrfi  9186  php3  9194  findcard3  9244  indexfi  9318  suppr  9433  infpr  9466  r111  9748  tcrank  9857  acndom  10036  infdif2  10193  infxpdom  10194  cfeq0  10241  cfsuc  10242  cfflb  10244  cflim2  10248  cfsmolem  10255  axcc3  10423  domtriomlem  10427  axdc3lem2  10436  axdc3lem4  10438  axdc4lem  10440  axcclem  10442  pwcfsdom  10569  tsktrss  10747  tsksuc  10748  tskuni  10769  adderpqlem  10940  mulerpqlem  10941  mulcanenq  10946  distrnq  10947  ltsonq  10955  ltanq  10957  ltmnq  10958  distrlem1pr  11011  distrlem5pr  11013  ltsopr  11018  ltsosr  11080  ltasr  11086  adddir  11198  axlttrn  11283  letr  11305  nnncan1  11495  npncan3  11497  pnpcan2  11499  subdi  11648  subdir  11649  mulcan1g  11868  mulcan2g  11869  divmul  11876  div23  11892  div13  11894  muldivdir  11908  divsubdir  11909  subdivcomb1  11911  divcan7  11925  ltmul2  12067  lemul1  12068  lemul2  12069  lemul2a  12071  lediv1  12081  ltmuldiv2  12090  lemuldiv  12096  lemuldiv2  12097  ltdiv2  12102  lediv2  12106  infrelb  12201  nndivtr  12284  bndndx  12504  nn0n0n1ge2  12573  fnn0ind  12696  addlelt  13133  xrletr  13184  qsqueeze  13228  xleadd2a  13281  xleadd1  13282  xltadd2  13284  xltmul2  13320  supxrbnd  13355  iooneg  13499  iccneg  13500  icoshft  13501  icoshftf1o  13502  zltaddlt1le  13533  fzen  13570  uzsubsubfz  13576  ssfzunsnext  13599  fzrevral2  13643  fzshftral  13645  fz0fzdiffz0  13667  elfzmlbp  13669  elfzo  13691  nelfzo  13695  fzoaddel2  13751  fzosubel2  13756  ssfzo12bi  13792  fzonfzoufzol  13802  subfzo0  13823  flltdivnn0lt  13868  modmulnn  13924  modcyc  13941  modaddabs  13946  modaddmod  13947  modmuladd  13951  modadd2mod  13959  modsubmod  13967  modsubmodmod  13968  modaddmodup  13972  modmulmod  13974  modsubdir  13978  modfzo0difsn  13981  modsumfzodifsn  13982  uzindi  14020  axdc4uzlem  14021  expneg2  14108  expdiv  14151  expubnd  14216  mulbinom2  14261  bernneq2  14268  expnngt1  14279  hashinfxadd  14423  hashunsngx  14431  hashunsnggt  14432  hashfundm  14481  hashf1dmcdm  14483  hashdifsnp1  14545  ccatval3  14618  ccatfv0  14623  ccatval1lsw  14624  ccats1val2  14667  ccatw2s1p1  14676  swrdnd  14694  pfxsuffeqwrdeq  14737  pfxsuff1eqwrdeq  14738  swrdswrd  14744  pfxpfx  14747  wrd2ind  14762  swrdccatin1  14764  pfxccatin12lem1  14767  swrdccatin2  14768  pfxccatin12lem3  14771  swrdccat  14774  pfxccatpfx1  14775  pfxccatpfx2  14776  swrdccat3blem  14778  repswswrd  14823  repswpfx  14824  repswccat  14825  cshwidxmod  14842  2cshw  14852  3cshw  14857  scshwfzeqfzo  14865  cshwcsh2id  14867  cshimadifsn  14868  cshimadifsn0  14869  ccatco  14874  cshco  14875  swrdco  14876  pfxco  14877  lswco  14878  swrds2  14979  2swrd2eqwrdeq  14992  shftuz  15108  sgn3da  15140  abs3dif  15385  fsumdifsnconst  15845  modfsummods  15847  sin02gt0  16249  dvdsval2  16314  dvdscmul  16341  dvdsmulc  16342  dvdscmulr  16343  dvdsmulcr  16344  divalglem8  16459  ndvdssub  16468  dvdsexpim  16614  rpmulgcd  16616  expgcd  16622  zexpgcd  16624  coprmprod  16720  cncongr1  16726  cncongr2  16727  isprm3  16742  modprm0  16866  coprimeprodsq  16869  pythagtriplem12  16887  pythagtriplem14  16889  pcprendvds  16901  pcmul  16912  pcdiv  16913  pcqcl  16917  pcqdiv  16918  pcdvdsb  16930  vdwnnlem1  17056  hashbcss  17065  cshwshashlem1  17156  fvsetsid  17229  setsstruct2  17235  setsstruct  17237  mrcss  17673  mrcsscl  17677  mrcun  17679  cofulid  17948  catcisolem  18168  funcsetcestrclem9  18220  latleeqj1  18508  lubun  18572  clatleglb  18575  pslem  18629  dirtr  18659  mgmb1mgm1  18714  pwspjmhm  18890  grpinvid1  19059  grpinvid2  19060  grpasscan1  19069  grpasscan2  19070  grpinvadd  19085  grpsubf  19086  grpsubrcan  19088  grpinvsub  19089  grpsubeq0  19093  grpsubadd0sub  19094  grppncan  19098  grpnpcan  19099  mulgnn0p1  19152  mulgaddcomlem  19164  mulginvcom  19166  mulginvinv  19167  subgsubcl  19205  subgsub  19206  eqglact  19248  qussub  19263  ghmsub  19295  psgnunilem4  19568  oddvds2  19637  odsubdvds  19642  gexnnod  19659  slwn0  19686  dvrcl  20487  unitdvcl  20488  dvrcan1  20492  dvrcan3  20493  dvreq1  20494  rngisom1  20549  rngisomring  20550  subrgdv  20675  abvsubtri  20911  idsrngd  20940  lmodvsubval2  21019  lsmcl  21185  lsmsp2  21189  lspsntrim  21200  rngqiprngimfolem  21411  lidldvgen  21483  cncrng  21524  chrcong  21658  dvdschrmulg  21659  zndvds  21680  zntoslem  21687  ocvsscon  21806  obselocv  21859  frlmphl  21912  ascldimul  22019  mpfsubrg  22243  ply1tmcl  22414  eqcoe1ply1eq  22440  gsummoncoe1  22449  lply1binomsc  22452  mamudm  22533  mamufacex  22534  scmatf1  22669  scmatf1o  22670  scmatrngiso  22674  submabas  22716  mdetdiaglem  22736  mdetralt2  22747  mdetero  22748  mdetunilem2  22751  mdetunilem6  22755  m2detleiblem7  22765  maducoeval2  22778  gsummatr01lem3  22795  gsummatr01  22797  smadiadetglem2  22810  cramerlem1  22825  mply1topmatcl  22943  mp2pm2mplem4  22947  ntrin  23199  elnei  23249  neindisj2  23261  ordtopn3  23334  leordtval2  23350  lecldbas  23357  cnrest2  23424  cmpsublem  23537  ptrescn  23777  xkococn  23798  kqfeq  23862  snfbas  24004  neifil  24018  fclsrest  24162  utopsnnei  24387  neipcfilu  24433  psmetsym  24448  psmetge0  24450  xmetge0  24482  xmetsym  24485  metustto  24691  metustbl  24704  restmetu  24708  nm2dif  24763  nmtri  24764  cnmet  24909  cnmpopc  25068  iihalf1  25071  iihalf2  25073  iocopnst  25080  clmnegsubdi2  25245  clmsub4  25246  clmvsubval2  25250  ncvspi  25296  cphsqrtcl3  25327  cph2ass  25353  cphipval2  25381  cphipval  25383  caublcls  25449  bcthlem3  25466  bcthlem4  25467  srabn  25500  cssbn  25515  cmslsschl  25517  rrxmet  25548  rrxdsfi  25551  iblconst  25958  dvdsq1p  26301  coeid3  26378  aannenlem2  26473  pserdvlem2  26572  tanord1  26683  cxpef  26811  recxpcl  26821  logbchbase  26917  relogbcl  26919  relogbzcl  26920  logbleb  26929  logblt  26930  relogbcxpb  26933  lawcos  26962  pythag  26963  isosctrlem1  26964  isosctrlem2  26965  lgsmodeq  27487  lgsmulsqcoprm  27488  gausslemma2dlem1a  27510  2lgsoddprmlem2  27554  ltsres  27807  lestr  27907  cofcutr  28098  lrrecpo  28115  ltadds2im  28160  leadds2im  28162  leadds1  28163  leadds2  28164  ltadds1  28166  addscan2  28167  addscan1  28168  ltsubs1  28250  divmulsw  28367  oldfib  28551  zsoring  28583  bdayfinbndlem1  28641  ax5seglem1  29259  axcontlem2  29296  axcontlem8  29302  upgrpredgv  29470  numedglnl  29475  issubgr2  29603  uhgrissubgr  29606  egrsubgr  29608  nbusgrfi  29705  nb3grprlem2  29712  cplgr3v  29766  cusgrsizeindslem  29782  finsumvtxdg2size  29881  rusgrpropadjvtx  29916  upgrwlkvtxedg  29975  usgr2trlncl  30090  uspgrn2crct  30138  crctcshwlkn0lem4  30143  crctcshwlkn0lem5  30144  wwlksnextproplem3  30241  umgr2adedgwlklem  30274  rusgr0edg  30306  clwwlk1loop  30320  clwwlkccatlem  30321  clwlkclwwlklem2a4  30329  clwlkclwwlklem2a  30330  clwwisshclwwslemlem  30345  erclwwlktr  30354  clwwlkel  30378  erclwwlkntr  30403  clwwlknonex2lem2  30440  uhgr3cyclex  30514  umgr3cyclex  30515  eucrctshift  30575  frgr3v  30607  3cyclfrgrrn  30618  frgrwopreglem5a  30643  frgr2wsp1  30662  extwwlkfab  30684  clwwlknonclwlknonf1o  30694  numclwwlk3lem1  30714  numclwwlk5  30720  numclwwlk6  30722  isgrpo  30830  grpoinvid1  30861  grpoinvid2  30862  grpoinvop  30866  grpodivinv  30869  grpoinvdiv  30870  grpodivf  30871  grponpcan  30876  ablonncan  30889  nvmval  30975  nvmval2  30976  nvmfval  30977  nvmul0or  30983  nvpncan2  30986  nvaddsub4  30990  nvmeq0  30991  nvdif  30999  nvpi  31000  nvmtri  31004  nvabs  31005  imsmetlem  31023  ipval2lem3  31038  ipval2  31040  4ipval2  31041  ipval3  31042  nmooge0  31100  blometi  31136  hvaddsub12  31371  hvsubdistr1  31382  hvsubdistr2  31383  hvaddcan2  31404  hvmulcan  31405  hvmulcan2  31406  hvsubcan  31407  hvsubcan2  31408  his7  31423  his2sub  31425  his2sub2  31426  norm3dif2  31484  shsubcl  31553  hhssnv  31597  shlej2  31694  fh2  31952  cm2j  31953  pjoi0  32050  hodcl  32080  hosubdi  32141  unopf1o  32249  unopadj  32252  adj2  32267  braadd  32278  bramul  32279  lnopaddmuli  32306  lnopsubmuli  32308  homco2  32310  lnfnaddmuli  32378  adjlnop  32419  leopmul  32467  leoptr  32470  pjimai  32509  atcv1  32713  atexch  32714  atcvatlem  32718  fcoinvbr  32931  preiman0  33036  divnumden2  33141  xdivmul  33225  cshf1o  33263  resvsca  33633  idlsrgcmnd  33786  hasheuni  34456  difelsiga  34504  cndprobin  34805  bayesth  34810  signstfvp  34939  breprexplemc  35000  trssfir1om  35488  fineqvac  35510  fineqvnttrclselem1  35515  fineqvnttrclselem3  35517  trssfir1omregs  35530  swrdrevpfx  35589  swrdwlk  35600  lediv2aALT  36150  fununiq  36242  dfrdg2  36266  clsun  36820  neiin  36824  rdgeqoa  37997  curfv  38232  matunitlindflem1  38248  poimirlem32  38284  ftc1anclem4  38328  areacirc  38345  filbcmb  38372  ismtybnd  38439  grpoeqdivid  38513  ghomco  38523  rngonegrmul  38576  zerdivemp1x  38579  rngohomco  38606  rngoisoco  38614  riscer  38620  intidl  38661  isfldidl  38700  eceldmqsxrncnvepres  39066  eceldmqsxrncnvepres2  39067  brredunds  39340  lshpnelb  39739  opnlen0  39943  opcon3b  39951  opcon2b  39952  oplecon3b  39955  opltcon3b  39959  opltcon2b  39961  oldmm1  39972  oldmm4  39975  oldmj1  39976  oldmj4  39979  cvrval2  40029  cvrcon3b  40032  leatb  40047  atcmp  40066  atcvreq0  40069  atlatle  40075  athgt  40211  3dim2  40223  islln2a  40272  lplnnleat  40297  lvolnleat  40338  4atlem10  40361  4atlem11  40364  4atlem12  40367  dalem21  40449  dalem22  40450  dalem23  40451  dalem29  40456  dalem30  40457  dalem31N  40458  dalem32  40459  dalem33  40460  dalem34  40461  dalem35  40462  dalem36  40463  dalem37  40464  dalem40  40467  dalem46  40473  dalem47  40474  dalem51  40478  dalem52  40479  dalem58  40485  dalem59  40486  pmaple  40516  paddclN  40597  pmapjoin  40607  pmapjat1  40608  elpcliN  40648  pclssN  40649  pclun2N  40654  2polcon4bN  40673  paddunN  40682  poldmj1N  40683  pmapj2N  40684  pmapocjN  40685  psubclinN  40703  paddatclN  40704  poml4N  40708  lautco  40852  ldilco  40871  ltrneq2  40903  trljat1  40921  cdlemc1  40946  cdleme10  41009  ltrnco  41474  trlcocnv  41475  trljco  41495  trljco2  41496  cdlemi1  41573  tendocnv  41776  diaord  41802  dibord  41914  dihord3  42012  dihord4  42013  dihmeetlem2N  42054  dihmeetlem4preN  42061  dochdmj1  42145  hdmap10lem  42594  lcmineqlem1  42777  sticksstones2  42895  readdsub  43126  reltsub1  43128  renpncan3  43133  reppncan  43135  resubdi  43138  readdcan2  43155  mzprename  43463  dvdsrabdioph  43520  pell14qrdivcl  43575  monotoddzz  43653  jm2.19lem2  43700  jm2.19  43703  relexpaddss  44427  k0004lem3  44858  dvconstbi  45027  chordthmALT  45624  isosctrlem1ALT  45625  ssinc  45788  ssdec  45789  wessf1ornlem  45886  disjf1o  45892  ssnnf1octb  45895  projf1o  45897  mapssbi  45912  iunmapsn  45916  upbdrech  46007  iuneqfzuzlem  46033  suplesup  46038  rexabslelem  46115  climxrrelem  46446  limsupresxr  46463  liminfresxr  46464  liminfvalxr  46480  xlimliminflimsup  46559  cncfshift  46571  cncfperiod  46576  cncfuni  46583  icccncfext  46584  dvmptfprodlem  46641  dvnprodlem1  46643  itgspltprt  46676  ismbl3  46683  stoweidlem3  46700  stoweidlem10  46707  stoweidlem19  46716  stoweidlem31  46728  stoweidlem34  46731  stoweidlem44  46741  fourierdlem41  46845  fourierdlem42  46846  fourierdlem51  46854  fourierdlem68  46871  fourierdlem89  46892  fourierdlem91  46894  fourierdlem92  46895  fourierdlem94  46897  etransclem24  46955  etransclem34  46965  qndenserrnbllem  46991  salincl  47021  saldifcl2  47025  subsalsal  47056  sge0pr  47091  sge0pnffigt  47093  sge0reuz  47144  nnfoctbdjlem  47152  nnfoctbdj  47153  meadjiunlem  47162  caratheodorylem2  47224  hoidmv1le  47291  hoidmvlelem3  47294  hspmbllem2  47324  opnvonmbllem2  47330  smfaddlem1  47460  sigaraf  47550  sigarmf  47551  nltle2tri  48033  subsubelfzo0  48047  nnmul2  48050  submodaddmod  48067  zplusmodne  48069  addmodne  48070  minusmod5ne  48075  submodneaddmod  48077  modmkpkne  48087  modmknepk  48088  iccpartiltu  48154  icceuelpart  48168  poprelb  48256  reuopreuprim  48258  nprmmul2  48260  proththd  48349  mogoldbblem  48468  fppr2odd  48479  fpprel2  48489  bgoldbtbndlem2  48554  clnbusgrfi  48591  grimuhgr  48635  uhgrimisgrgric  48679  clnbgrgrim  48682  grtrif1o  48690  grlimgrtri  48751  gpgusgralem  48804  gpgedgvtx0  48809  gpgedg2ov  48814  gpgedg2iv  48815  gpg5nbgrvtx03starlem2  48817  nn0sumltlt  49113  invginvrid  49130  ply1sclrmsm  49147  linccl  49177  lincvalpr  49181  lincresunit3lem1  49242  lincresunit3  49244  fdivmpt  49303  nnolog2flm1  49353  dignnld  49366  digexp  49370  dignn0flhalflem1  49378  itcovalsucov  49431  reorelicc  49473  eenglngeehlnmlem1  49500  line2  49515  line2xlem  49516  itsclc0lem1  49519  itsclc0xyqsolr  49532  i0oii  49681  io1ii  49682  indthinc  50223  indthincALT  50224  setrec2fun  50453  reccot  50519  rectan  50520