Theorem 3adant2 1147

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 1125	1 ⊢ ((𝜑 ∧ 𝜃 ∧ 𝜓) → 𝜒)

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

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 1103

This theorem is referenced by:  3ad2ant1  1149  3simpb  1165  3imp3i2an  1362  eupickb  2665  eqeu  3672  onunel  6457  iotan0  6515  funopg  6559  dff1o2  6816  fvelimad  6938  unima  6946  fnimapr  6954  fvmptt  7000  fnreseql  7033  xpprsng  7126  f1elima  7251  f1ounsn  7260  f13dfv  7262  f1ocnvfvb  7267  f1cdmsn  7270  f1ofvswap  7294  oprssov  7569  resf1extb  7919  resf1ext2b  7920  funelss  8032  poxp  8112  poxp2  8127  poxp3  8134  smoiso  8337  oaord  8520  oaword  8522  omcan  8542  omwordri  8545  odi  8552  omeulem1  8555  oeord  8562  oecan  8563  oewordri  8566  oeordsuc  8568  nnaord  8593  nnaordr  8594  nndi  8597  nnaword  8601  nnmwordri  8610  naddel2  8663  naddss1  8664  naddss2  8665  erov  8800  ecopovtrn  8806  mapsnd  8872  f1dom3g  8952  xpdom3  9051  mapxpen  9119  dif1en  9134  findcard  9136  f1domfi2  9154  entrfir  9163  domtrfil  9164  domtrfir  9166  sbthfilem  9170  sdomdomtrfi  9173  php3  9181  findcard3  9231  indexfi  9305  suppr  9420  infpr  9453  r111  9735  tcrank  9844  acndom  10023  infdif2  10180  infxpdom  10181  cfeq0  10228  cfsuc  10229  cfflb  10231  cflim2  10235  cfsmolem  10242  axcc3  10410  domtriomlem  10414  axdc3lem2  10423  axdc3lem4  10425  axdc4lem  10427  axcclem  10429  pwcfsdom  10556  tsktrss  10734  tsksuc  10735  tskuni  10756  adderpqlem  10927  mulerpqlem  10928  mulcanenq  10933  distrnq  10934  ltsonq  10942  ltanq  10944  ltmnq  10945  distrlem1pr  10998  distrlem5pr  11000  ltsopr  11005  ltsosr  11067  ltasr  11073  adddir  11185  axlttrn  11270  letr  11292  nnncan1  11482  npncan3  11484  pnpcan2  11486  subdi  11635  subdir  11636  mulcan1g  11855  mulcan2g  11856  divmul  11863  div23  11879  div13  11881  muldivdir  11895  divsubdir  11896  subdivcomb1  11898  divcan7  11912  ltmul2  12054  lemul1  12055  lemul2  12056  lemul2a  12058  lediv1  12068  ltmuldiv2  12077  lemuldiv  12083  lemuldiv2  12084  ltdiv2  12089  lediv2  12093  infrelb  12188  nndivtr  12271  bndndx  12491  nn0n0n1ge2  12560  fnn0ind  12683  addlelt  13120  xrletr  13171  qsqueeze  13215  xleadd2a  13268  xleadd1  13269  xltadd2  13271  xltmul2  13307  supxrbnd  13342  iooneg  13486  iccneg  13487  icoshft  13488  icoshftf1o  13489  zltaddlt1le  13520  fzen  13557  uzsubsubfz  13562  ssfzunsnext  13585  fzrevral2  13629  fzshftral  13631  fz0fzdiffz0  13653  elfzmlbp  13655  elfzo  13677  nelfzo  13681  fzoaddel2  13737  fzosubel2  13742  ssfzo12bi  13778  fzonfzoufzol  13788  subfzo0  13809  flltdivnn0lt  13854  modmulnn  13910  modcyc  13927  modaddabs  13932  modaddmod  13933  modmuladd  13937  modadd2mod  13945  modsubmod  13953  modsubmodmod  13954  modaddmodup  13958  modmulmod  13960  modsubdir  13964  modfzo0difsn  13967  modsumfzodifsn  13968  uzindi  14006  axdc4uzlem  14007  expneg2  14094  expdiv  14137  expubnd  14202  mulbinom2  14247  bernneq2  14254  expnngt1  14265  hashinfxadd  14409  hashunsngx  14417  hashunsnggt  14418  hashfundm  14467  hashf1dmcdm  14469  hashdifsnp1  14531  ccatval3  14604  ccatfv0  14609  ccatval1lsw  14610  ccats1val2  14653  ccatw2s1p1  14662  swrdnd  14680  pfxsuffeqwrdeq  14723  pfxsuff1eqwrdeq  14724  swrdswrd  14730  pfxpfx  14733  wrd2ind  14748  swrdccatin1  14750  pfxccatin12lem1  14753  swrdccatin2  14754  pfxccatin12lem3  14757  swrdccat  14760  pfxccatpfx1  14761  pfxccatpfx2  14762  swrdccat3blem  14764  repswswrd  14809  repswpfx  14810  repswccat  14811  cshwidxmod  14828  2cshw  14838  3cshw  14843  scshwfzeqfzo  14851  cshwcsh2id  14853  cshimadifsn  14854  cshimadifsn0  14855  ccatco  14860  cshco  14861  swrdco  14862  pfxco  14863  lswco  14864  swrds2  14965  2swrd2eqwrdeq  14978  shftuz  15094  sgn3da  15126  abs3dif  15371  fsumdifsnconst  15831  modfsummods  15833  sin02gt0  16236  dvdsval2  16301  dvdscmul  16328  dvdsmulc  16329  dvdscmulr  16330  dvdsmulcr  16331  divalglem8  16446  ndvdssub  16455  dvdsexpim  16601  rpmulgcd  16603  expgcd  16609  zexpgcd  16611  coprmprod  16707  cncongr1  16713  cncongr2  16714  isprm3  16729  modprm0  16853  coprimeprodsq  16856  pythagtriplem12  16874  pythagtriplem14  16876  pcprendvds  16888  pcmul  16899  pcdiv  16900  pcqcl  16904  pcqdiv  16905  pcdvdsb  16917  vdwnnlem1  17043  hashbcss  17052  cshwshashlem1  17143  fvsetsid  17216  setsstruct2  17222  setsstruct  17224  mrcss  17660  mrcsscl  17664  mrcun  17666  cofulid  17935  catcisolem  18155  funcsetcestrclem9  18207  latleeqj1  18495  lubun  18559  clatleglb  18562  pslem  18616  dirtr  18646  mgmb1mgm1  18701  pwspjmhm  18877  grpinvid1  19046  grpinvid2  19047  grpasscan1  19056  grpasscan2  19057  grpinvadd  19072  grpsubf  19073  grpsubrcan  19075  grpinvsub  19076  grpsubeq0  19080  grpsubadd0sub  19081  grppncan  19085  grpnpcan  19086  mulgnn0p1  19139  mulgaddcomlem  19151  mulginvcom  19153  mulginvinv  19154  subgsubcl  19192  subgsub  19193  eqglact  19235  qussub  19250  ghmsub  19282  psgnunilem4  19555  oddvds2  19624  odsubdvds  19629  gexnnod  19646  slwn0  19673  dvrcl  20474  unitdvcl  20475  dvrcan1  20479  dvrcan3  20480  dvreq1  20481  rngisom1  20536  rngisomring  20537  subrgdv  20662  abvsubtri  20896  idsrngd  20925  lmodvsubval2  21004  lsmcl  21170  lsmsp2  21174  lspsntrim  21185  rngqiprngimfolem  21389  lidldvgen  21459  cncrng  21500  chrcong  21634  dvdschrmulg  21635  zndvds  21656  zntoslem  21663  ocvsscon  21782  obselocv  21835  frlmphl  21888  ascldimul  21995  mpfsubrg  22219  ply1tmcl  22390  eqcoe1ply1eq  22416  gsummoncoe1  22425  lply1binomsc  22428  mamudm  22509  mamufacex  22510  scmatf1  22645  scmatf1o  22646  scmatrngiso  22650  submabas  22692  mdetdiaglem  22712  mdetralt2  22723  mdetero  22724  mdetunilem2  22727  mdetunilem6  22731  m2detleiblem7  22741  maducoeval2  22754  gsummatr01lem3  22771  gsummatr01  22773  smadiadetglem2  22786  cramerlem1  22801  mply1topmatcl  22919  mp2pm2mplem4  22923  ntrin  23175  elnei  23225  neindisj2  23237  ordtopn3  23310  leordtval2  23326  lecldbas  23333  cnrest2  23400  cmpsublem  23513  ptrescn  23753  xkococn  23774  kqfeq  23838  snfbas  23980  neifil  23994  fclsrest  24138  utopsnnei  24363  neipcfilu  24409  psmetsym  24424  psmetge0  24426  xmetge0  24458  xmetsym  24461  metustto  24667  metustbl  24680  restmetu  24684  nm2dif  24739  nmtri  24740  cnmet  24885  cnmpopc  25044  iihalf1  25047  iihalf2  25049  iocopnst  25056  clmnegsubdi2  25221  clmsub4  25222  clmvsubval2  25226  ncvspi  25272  cphsqrtcl3  25303  cph2ass  25329  cphipval2  25357  cphipval  25359  caublcls  25425  bcthlem3  25442  bcthlem4  25443  srabn  25476  cssbn  25491  cmslsschl  25493  rrxmet  25524  rrxdsfi  25527  iblconst  25934  dvdsq1p  26277  coeid3  26354  aannenlem2  26447  pserdvlem2  26545  tanord1  26656  cxpef  26784  recxpcl  26794  logbchbase  26890  relogbcl  26892  relogbzcl  26893  logbleb  26902  logblt  26903  relogbcxpb  26906  lawcos  26935  pythag  26936  isosctrlem1  26937  isosctrlem2  26938  lgsmodeq  27460  lgsmulsqcoprm  27461  gausslemma2dlem1a  27483  2lgsoddprmlem2  27527  ltsres  27780  lestr  27880  cofcutr  28071  lrrecpo  28088  ltadds2im  28133  leadds2im  28135  leadds1  28136  leadds2  28137  ltadds1  28139  addscan2  28140  addscan1  28141  ltsubs1  28223  divmulsw  28340  oldfib  28524  zsoring  28556  bdayfinbndlem1  28614  ax5seglem1  29183  axcontlem2  29220  axcontlem8  29226  upgrpredgv  29394  numedglnl  29399  issubgr2  29527  uhgrissubgr  29530  egrsubgr  29532  nbusgrfi  29629  nb3grprlem2  29636  cplgr3v  29690  cusgrsizeindslem  29706  finsumvtxdg2size  29805  rusgrpropadjvtx  29840  upgrwlkvtxedg  29899  usgr2trlncl  30014  uspgrn2crct  30062  crctcshwlkn0lem4  30067  crctcshwlkn0lem5  30068  wwlksnextproplem3  30165  umgr2adedgwlklem  30198  rusgr0edg  30230  clwwlk1loop  30244  clwwlkccatlem  30245  clwlkclwwlklem2a4  30253  clwlkclwwlklem2a  30254  clwwisshclwwslemlem  30269  erclwwlktr  30278  clwwlkel  30302  erclwwlkntr  30327  clwwlknonex2lem2  30364  uhgr3cyclex  30438  umgr3cyclex  30439  eucrctshift  30499  frgr3v  30531  3cyclfrgrrn  30542  frgrwopreglem5a  30567  frgr2wsp1  30586  extwwlkfab  30608  clwwlknonclwlknonf1o  30618  numclwwlk3lem1  30638  numclwwlk5  30644  numclwwlk6  30646  isgrpo  30754  grpoinvid1  30785  grpoinvid2  30786  grpoinvop  30790  grpodivinv  30793  grpoinvdiv  30794  grpodivf  30795  grponpcan  30800  ablonncan  30813  nvmval  30899  nvmval2  30900  nvmfval  30901  nvmul0or  30907  nvpncan2  30910  nvaddsub4  30914  nvmeq0  30915  nvdif  30923  nvpi  30924  nvmtri  30928  nvabs  30929  imsmetlem  30947  ipval2lem3  30962  ipval2  30964  4ipval2  30965  ipval3  30966  nmooge0  31024  blometi  31060  hvaddsub12  31295  hvsubdistr1  31306  hvsubdistr2  31307  hvaddcan2  31328  hvmulcan  31329  hvmulcan2  31330  hvsubcan  31331  hvsubcan2  31332  his7  31347  his2sub  31349  his2sub2  31350  norm3dif2  31408  shsubcl  31477  hhssnv  31521  shlej2  31618  fh2  31876  cm2j  31877  pjoi0  31974  hodcl  32004  hosubdi  32065  unopf1o  32173  unopadj  32176  adj2  32191  braadd  32202  bramul  32203  lnopaddmuli  32230  lnopsubmuli  32232  homco2  32234  lnfnaddmuli  32302  adjlnop  32343  leopmul  32391  leoptr  32394  pjimai  32433  atcv1  32637  atexch  32638  atcvatlem  32642  fcoinvbr  32856  preiman0  32963  divnumden2  33068  xdivmul  33152  cshf1o  33190  resvsca  33562  idlsrgcmnd  33717  hasheuni  34387  difelsiga  34435  cndprobin  34736  bayesth  34741  signstfvp  34870  breprexplemc  34931  trssfir1om  35414  fineqvac  35419  fineqvnttrclselem1  35424  fineqvnttrclselem3  35426  trssfir1omregs  35439  swrdrevpfx  35474  swrdwlk  35485  lediv2aALT  36035  fununiq  36127  dfrdg2  36151  clsun  36696  neiin  36700  rdgeqoa  37871  curfv  38106  matunitlindflem1  38122  poimirlem32  38158  ftc1anclem4  38202  areacirc  38219  filbcmb  38246  ismtybnd  38313  grpoeqdivid  38387  ghomco  38397  rngonegrmul  38450  zerdivemp1x  38453  rngohomco  38480  rngoisoco  38488  riscer  38494  intidl  38535  isfldidl  38574  eceldmqsxrncnvepres  38942  eceldmqsxrncnvepres2  38943  brredunds  39216  lshpnelb  39615  opnlen0  39819  opcon3b  39827  opcon2b  39828  oplecon3b  39831  opltcon3b  39835  opltcon2b  39837  oldmm1  39848  oldmm4  39851  oldmj1  39852  oldmj4  39855  cvrval2  39905  cvrcon3b  39908  leatb  39923  atcmp  39942  atcvreq0  39945  atlatle  39951  athgt  40087  3dim2  40099  islln2a  40148  lplnnleat  40173  lvolnleat  40214  4atlem10  40237  4atlem11  40240  4atlem12  40243  dalem21  40325  dalem22  40326  dalem23  40327  dalem29  40332  dalem30  40333  dalem31N  40334  dalem32  40335  dalem33  40336  dalem34  40337  dalem35  40338  dalem36  40339  dalem37  40340  dalem40  40343  dalem46  40349  dalem47  40350  dalem51  40354  dalem52  40355  dalem58  40361  dalem59  40362  pmaple  40392  paddclN  40473  pmapjoin  40483  pmapjat1  40484  elpcliN  40524  pclssN  40525  pclun2N  40530  2polcon4bN  40549  paddunN  40558  poldmj1N  40559  pmapj2N  40560  pmapocjN  40561  psubclinN  40579  paddatclN  40580  poml4N  40584  lautco  40728  ldilco  40747  ltrneq2  40779  trljat1  40797  cdlemc1  40822  cdleme10  40885  ltrnco  41350  trlcocnv  41351  trljco  41371  trljco2  41372  cdlemi1  41449  tendocnv  41652  diaord  41678  dibord  41790  dihord3  41888  dihord4  41889  dihmeetlem2N  41930  dihmeetlem4preN  41937  dochdmj1  42021  hdmap10lem  42470  lcmineqlem1  42653  sticksstones2  42771  readdsub  43000  reltsub1  43002  renpncan3  43007  reppncan  43009  resubdi  43012  readdcan2  43029  mzprename  43337  dvdsrabdioph  43394  pell14qrdivcl  43449  monotoddzz  43527  jm2.19lem2  43574  jm2.19  43577  relexpaddss  44301  k0004lem3  44732  dvconstbi  44903  chordthmALT  45500  isosctrlem1ALT  45501  ssinc  45664  ssdec  45665  wessf1ornlem  45762  disjf1o  45768  ssnnf1octb  45771  projf1o  45773  mapssbi  45788  iunmapsn  45792  upbdrech  45883  iuneqfzuzlem  45909  suplesup  45914  rexabslelem  45991  climxrrelem  46322  limsupresxr  46339  liminfresxr  46340  liminfvalxr  46356  xlimliminflimsup  46435  cncfshift  46447  cncfperiod  46452  cncfuni  46459  icccncfext  46460  dvmptfprodlem  46517  dvnprodlem1  46519  itgspltprt  46552  ismbl3  46559  stoweidlem3  46576  stoweidlem10  46583  stoweidlem19  46592  stoweidlem31  46604  stoweidlem34  46607  stoweidlem44  46617  fourierdlem41  46721  fourierdlem42  46722  fourierdlem51  46730  fourierdlem68  46747  fourierdlem89  46768  fourierdlem91  46770  fourierdlem92  46771  fourierdlem94  46773  etransclem24  46831  etransclem34  46841  qndenserrnbllem  46867  salincl  46897  saldifcl2  46901  subsalsal  46932  sge0pr  46967  sge0pnffigt  46969  sge0reuz  47020  nnfoctbdjlem  47028  nnfoctbdj  47029  meadjiunlem  47038  caratheodorylem2  47100  hoidmv1le  47167  hoidmvlelem3  47170  hspmbllem2  47200  opnvonmbllem2  47206  smfaddlem1  47336  sigaraf  47426  sigarmf  47427  nltle2tri  47906  subsubelfzo0  47920  nnmul2  47923  submodaddmod  47940  zplusmodne  47942  addmodne  47943  minusmod5ne  47948  submodneaddmod  47950  modmkpkne  47960  modmknepk  47961  iccpartiltu  48027  icceuelpart  48041  poprelb  48129  reuopreuprim  48131  nprmmul2  48133  proththd  48222  mogoldbblem  48341  fppr2odd  48352  fpprel2  48362  bgoldbtbndlem2  48427  clnbusgrfi  48464  grimuhgr  48508  uhgrimisgrgric  48552  clnbgrgrim  48555  grtrif1o  48563  grlimgrtri  48624  gpgusgralem  48677  gpgedgvtx0  48682  gpgedg2ov  48687  gpgedg2iv  48688  gpg5nbgrvtx03starlem2  48690  nn0sumltlt  48982  invginvrid  48999  ply1sclrmsm  49016  linccl  49046  lincvalpr  49050  lincresunit3lem1  49111  lincresunit3  49113  fdivmpt  49172  nnolog2flm1  49222  dignnld  49235  digexp  49239  dignn0flhalflem1  49247  itcovalsucov  49300  reorelicc  49342  eenglngeehlnmlem1  49369  line2  49384  line2xlem  49385  itsclc0lem1  49388  itsclc0xyqsolr  49401  i0oii  49550  io1ii  49551  indthinc  50092  indthincALT  50093  setrec2fun  50322  reccot  50388  rectan  50389