Theorem simp2 1022

Description: Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)

Assertion

Ref	Expression
simp2	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓)

Proof of Theorem simp2

Step	Hyp	Ref	Expression
1		3simpa 1018	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜑 ∧ 𝜓))
2	1	simprd 114	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓)

Syntax hints:   → wi 4   ∧ w3a 1002

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This theorem depends on definitions:  df-bi 117  df-3an 1004

This theorem is referenced by:  simpl2  1025  simpr2  1028  simp2i  1031  simp2d  1034  simp12  1052  simp22  1055  simp32  1058  syld3an3  1316  3ianorr  1343  intn3an2d  1391  stoic4b  1475  nlim0  4485  tfisi  4679  sotri2  5126  sotri3  5127  feq123  5465  sefvex  5650  fvmptt  5728  fnfvima  5878  cocan1  5917  cocan2  5918  ovexg  6041  ovmpox  6139  ovmpoga  6140  fvmpopr2d  6147  caovimo  6205  tfr1onlembxssdm  6495  tfr1onlembfn  6496  tfrcllembxssdm  6508  tfrcllembfn  6509  freccllem  6554  frecfcllem  6556  frecsuclem  6558  frecrdg  6560  domssr  6937  mapxpen  7017  dif1en  7049  diffifi  7064  unsnfidcex  7090  unfidisj  7092  undifdc  7094  resfnfinfinss  7114  funrnfi  7117  sbthlemi9  7140  elfir  7148  difinfsn  7275  ctssdc  7288  djuassen  7407  xpdjuen  7408  mulcanenq  7580  ltanqg  7595  mulcanenq0ec  7640  addnnnq0  7644  distrprg  7783  aptipr  7836  addsrpr  7940  mulsrpr  7941  mulasssrg  7953  ltpsrprg  7998  axmulass  8068  axpre-ltadd  8081  subadd2  8358  nppcan  8376  nppcan3  8378  subsub2  8382  subsub4  8387  npncan3  8392  pnpcan  8393  pnncan  8395  subcan  8409  ltadd1  8584  leadd1  8585  leadd2  8586  ltsubadd  8587  ltsubadd2  8588  lesubadd  8589  lesubadd2  8590  ltaddsub  8591  leaddsub  8593  lesub1  8611  lesub2  8612  ltsub1  8613  ltsub2  8614  gt0add  8728  apreap  8742  lemul1  8748  reapmul1lem  8749  reapmul1  8750  reapadd1  8751  remulext1  8754  remulext2  8755  apadd2  8764  mulext2  8768  mulap0r  8770  leltap  8780  ltap  8788  apsub1  8797  recexaplem2  8807  mulcanap  8820  mulcanap2  8821  divvalap  8829  divmulap  8830  divcanap1  8836  diveqap0  8837  divap0b  8838  divrecap  8843  divassap  8845  div23ap  8846  divdirap  8852  divcanap3  8853  div11ap  8855  diveqap1  8860  divmuldivap  8867  divcanap5  8869  redivclap  8886  div2negap  8890  apmul1  8943  apmul2  8944  div2subap  8992  ltdiv1  9023  ledivmul  9032  lemuldiv  9036  lt2msq1  9040  ltdiv23  9047  squeeze0  9059  ofnegsub  9117  zaddcllemneg  9493  eluzsub  9760  nn01to3  9820  rpgecl  9886  addlelt  9972  xleadd1  10079  xltadd1  10080  lbioog  10117  ubioc1  10133  ubicc2  10189  icoshftf1o  10195  fzen  10247  nelfzo  10356  ubmelfzo  10414  ssfzo12  10438  ubmelm1fzo  10440  fzosplitprm1  10448  zsupssdc  10466  rebtwn2zlemshrink  10481  qbtwnre  10484  icogelb  10493  flqwordi  10516  flqword2  10517  flltdivnn0lt  10532  modqcl  10556  mulqmod0  10560  modqmulnn  10572  modqabs2  10588  modqmuladdnn0  10598  qnegmod  10599  addmodid  10602  modqm1p1mod0  10605  modifeq2int  10616  modqdi  10622  modqeqmodmin  10624  modfzo0difsn  10625  frec2uzf1od  10636  exp3val  10771  expnegap0  10777  expgt1  10807  exprecap  10810  expmulzap  10815  leexp2a  10822  expubnd  10826  mulbinom2  10886  bernneq2  10891  expnbnd  10893  fihashss  11046  fihashssdif  11048  fimaxq  11057  ccatval2  11141  ccatass  11151  swrdval  11188  swrdnd  11199  pfxfv  11224  pfxpfx  11248  ccats1pfxeq  11254  ccats1pfxeqrex  11255  s3cl  11326  s3fv0g  11331  s3fv1g  11332  shftuz  11336  shftfibg  11339  cjdivap  11428  resqrtcl  11548  absdivap  11589  abssubne0  11610  maxleast  11732  lemininf  11753  ltmininf  11754  xrmaxltsup  11777  xrmaxaddlem  11779  xrmaxadd  11780  xrmineqinf  11788  xrltmininf  11789  xrminltinf  11791  xrminadd  11794  climuni  11812  reccn2ap  11832  isumz  11908  geoisum1c  12039  prod1dc  12105  efltim  12217  dvdsval2  12309  dvdscmulr  12339  dvdsmulcr  12340  modmulconst  12342  dvdsadd2b  12359  dvdsexp  12380  mulmoddvds  12382  divalglemeuneg  12442  gcdaddm  12513  dvdsgcdb  12542  mulgcd  12545  gcddiv  12548  uzwodc  12566  lcmdvdsb  12614  mulgcddvds  12624  qredeq  12626  divgcdcoprm0  12631  cncongr1  12633  euclemma  12676  rpexp  12683  rpexp12i  12685  fermltl  12764  prmdiv  12765  odzcllem  12773  odzdvds  12776  odzphi  12777  vfermltl  12782  coprimeprodsq  12788  pythagtriplem6  12801  pythagtriplem7  12802  pythagtriplem12  12806  pythagtriplem13  12807  pceu  12826  pcdvdsb  12851  pcgcd1  12859  dvdsprmpweq  12866  sumhashdc  12878  ctinf  13009  fvsetsid  13074  ressressg  13116  ressabsg  13117  rngplusgg  13178  imasaddvallemg  13356  qusaddvallemg  13374  plusfvalg  13404  mgmb1mgm1  13409  issubmnd  13483  ress0g  13484  imasmnd2  13493  imasmnd  13494  gsumfzz  13536  grpasscan2  13605  grpidrcan  13606  grpidlcan  13607  grpinvadd  13619  grpsubeq0  13627  grppncan  13632  dfgrp3mlem  13639  dfgrp3me  13641  grpsubpropd2  13646  pwsinvg  13653  imasgrp2  13655  imasgrp  13656  mhmmnd  13661  mulgnn0p1  13678  mulgnnsubcl  13679  mulgnn0subcl  13680  mulgsubcl  13681  mulgneg  13685  mulgaddcom  13691  mulginvcom  13692  submmulg  13711  subgcl  13729  subgsubcl  13730  subgsub  13731  subgmulg  13733  nsgconj  13751  nsgid  13760  quseccl0g  13776  ghmmulg  13801  ghmeqker  13816  f1ghm0to0  13817  kerf1ghm  13819  ablinvadd  13855  ablsub4  13858  ablpncan2  13861  subgabl  13877  gsumfzconst  13886  rngcl  13915  imasrng  13927  srgcl  13941  ringcl  13984  crngcom  13985  ringidss  14000  ringcom  14002  imasring  14035  opprringbg  14051  unitmulcl  14085  unitmulclb  14086  dvrcl  14107  unitdvcl  14108  dvrcan1  14112  dvrcan3  14113  rhmmul  14136  subrngrng  14174  subrngmcl  14181  subrgmcl  14205  subrgdv  14210  rrgeq0  14237  domneq0  14244  islmod  14263  scafvalg  14279  lmodcom  14305  rmodislmodlem  14322  rmodislmod  14323  lssclg  14336  lssvnegcl  14348  lssintclm  14356  lspss  14371  lspun  14374  lspsnvsi  14390  rspssp  14466  rnglidlmmgm  14468  rnglidlmsgrp  14469  rnglidlrng  14470  zndvds  14621  2basgeng  14764  iuncld  14797  ntrss  14801  restco  14856  restabs  14857  cnprcl2k  14888  lmconst  14898  cnrest2  14918  cnmpt2t  14975  psmetsym  15011  psmetge0  15013  xmetge0  15047  xmetsym  15050  blvalps  15070  blval  15071  xblcntrps  15095  xblcntr  15096  xmssym  15151  blsscls2  15175  bdxmet  15183  txmetcnp  15200  dvfvalap  15363  dvid  15377  dvidre  15379  dvcnp2cntop  15381  elplyr  15422  rpcxpadd  15587  rpcxpsub  15590  rpmulcxp  15591  rpdivcxp  15593  cxpmul  15594  rpcxple2  15600  rpcxplt2  15601  rplogbval  15627  rplogbcl  15628  rplogbreexp  15635  relogbexpap  15640  logbleb  15643  logblt  15644  rplogbcxp  15645  rpcxplogb  15646  relogbcxpbap  15647  sgmppw  15674  lgsneg1  15712  lgsmod  15713  lgsne0  15725  lgssq  15727  lgsdirnn0  15734  lgsdinn0  15735  lgsquad  15767  funvtxvalg  15845  funiedgvalg  15846  lpvtx  15887  ausgrumgrien  15976  ausgrusgrien  15977  wlkl1loop  16079  findset  16332