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  4486  tfisi  4680  sotri2  5129  sotri3  5130  feq123  5468  sefvex  5653  fvmptt  5731  fnfvima  5881  cocan1  5920  cocan2  5921  ovexg  6044  ovmpox  6142  ovmpoga  6143  fvmpopr2d  6150  caovimo  6208  tfr1onlembxssdm  6500  tfr1onlembfn  6501  tfrcllembxssdm  6513  tfrcllembfn  6514  freccllem  6559  frecfcllem  6561  frecsuclem  6563  frecrdg  6565  domssr  6942  mapxpen  7022  dif1en  7054  diffifi  7069  unsnfidcex  7098  unfidisj  7100  undifdc  7102  resfnfinfinss  7122  funrnfi  7125  sbthlemi9  7148  elfir  7156  difinfsn  7283  ctssdc  7296  djuassen  7415  xpdjuen  7416  mulcanenq  7588  ltanqg  7603  mulcanenq0ec  7648  addnnnq0  7652  distrprg  7791  aptipr  7844  addsrpr  7948  mulsrpr  7949  mulasssrg  7961  ltpsrprg  8006  axmulass  8076  axpre-ltadd  8089  subadd2  8366  nppcan  8384  nppcan3  8386  subsub2  8390  subsub4  8395  npncan3  8400  pnpcan  8401  pnncan  8403  subcan  8417  ltadd1  8592  leadd1  8593  leadd2  8594  ltsubadd  8595  ltsubadd2  8596  lesubadd  8597  lesubadd2  8598  ltaddsub  8599  leaddsub  8601  lesub1  8619  lesub2  8620  ltsub1  8621  ltsub2  8622  gt0add  8736  apreap  8750  lemul1  8756  reapmul1lem  8757  reapmul1  8758  reapadd1  8759  remulext1  8762  remulext2  8763  apadd2  8772  mulext2  8776  mulap0r  8778  leltap  8788  ltap  8796  apsub1  8805  recexaplem2  8815  mulcanap  8828  mulcanap2  8829  divvalap  8837  divmulap  8838  divcanap1  8844  diveqap0  8845  divap0b  8846  divrecap  8851  divassap  8853  div23ap  8854  divdirap  8860  divcanap3  8861  div11ap  8863  diveqap1  8868  divmuldivap  8875  divcanap5  8877  redivclap  8894  div2negap  8898  apmul1  8951  apmul2  8952  div2subap  9000  ltdiv1  9031  ledivmul  9040  lemuldiv  9044  lt2msq1  9048  ltdiv23  9055  squeeze0  9067  ofnegsub  9125  zaddcllemneg  9501  eluzsub  9769  nn01to3  9829  rpgecl  9895  addlelt  9981  xleadd1  10088  xltadd1  10089  lbioog  10126  ubioc1  10142  ubicc2  10198  icoshftf1o  10204  fzen  10256  nelfzo  10365  ubmelfzo  10423  ssfzo12  10447  ubmelm1fzo  10449  fzosplitprm1  10457  zsupssdc  10475  rebtwn2zlemshrink  10490  qbtwnre  10493  icogelb  10502  flqwordi  10525  flqword2  10526  flltdivnn0lt  10541  modqcl  10565  mulqmod0  10569  modqmulnn  10581  modqabs2  10597  modqmuladdnn0  10607  qnegmod  10608  addmodid  10611  modqm1p1mod0  10614  modifeq2int  10625  modqdi  10631  modqeqmodmin  10633  modfzo0difsn  10634  frec2uzf1od  10645  exp3val  10780  expnegap0  10786  expgt1  10816  exprecap  10819  expmulzap  10824  leexp2a  10831  expubnd  10835  mulbinom2  10895  bernneq2  10900  expnbnd  10902  fihashss  11056  fihashssdif  11058  fimaxq  11067  ccatval2  11151  ccatass  11161  swrdval  11201  swrdnd  11212  pfxfv  11237  pfxpfx  11261  ccats1pfxeq  11267  ccats1pfxeqrex  11268  s3cl  11339  s3fv0g  11344  s3fv1g  11345  shftuz  11349  shftfibg  11352  cjdivap  11441  resqrtcl  11561  absdivap  11602  abssubne0  11623  maxleast  11745  lemininf  11766  ltmininf  11767  xrmaxltsup  11790  xrmaxaddlem  11792  xrmaxadd  11793  xrmineqinf  11801  xrltmininf  11802  xrminltinf  11804  xrminadd  11807  climuni  11825  reccn2ap  11845  isumz  11921  geoisum1c  12052  prod1dc  12118  efltim  12230  dvdsval2  12322  dvdscmulr  12352  dvdsmulcr  12353  modmulconst  12355  dvdsadd2b  12372  dvdsexp  12393  mulmoddvds  12395  divalglemeuneg  12455  gcdaddm  12526  dvdsgcdb  12555  mulgcd  12558  gcddiv  12561  uzwodc  12579  lcmdvdsb  12627  mulgcddvds  12637  qredeq  12639  divgcdcoprm0  12644  cncongr1  12646  euclemma  12689  rpexp  12696  rpexp12i  12698  fermltl  12777  prmdiv  12778  odzcllem  12786  odzdvds  12789  odzphi  12790  vfermltl  12795  coprimeprodsq  12801  pythagtriplem6  12814  pythagtriplem7  12815  pythagtriplem12  12819  pythagtriplem13  12820  pceu  12839  pcdvdsb  12864  pcgcd1  12872  dvdsprmpweq  12879  sumhashdc  12891  ctinf  13022  fvsetsid  13087  ressressg  13129  ressabsg  13130  rngplusgg  13191  imasaddvallemg  13369  qusaddvallemg  13387  plusfvalg  13417  mgmb1mgm1  13422  issubmnd  13496  ress0g  13497  imasmnd2  13506  imasmnd  13507  gsumfzz  13549  grpasscan2  13618  grpidrcan  13619  grpidlcan  13620  grpinvadd  13632  grpsubeq0  13640  grppncan  13645  dfgrp3mlem  13652  dfgrp3me  13654  grpsubpropd2  13659  pwsinvg  13666  imasgrp2  13668  imasgrp  13669  mhmmnd  13674  mulgnn0p1  13691  mulgnnsubcl  13692  mulgnn0subcl  13693  mulgsubcl  13694  mulgneg  13698  mulgaddcom  13704  mulginvcom  13705  submmulg  13724  subgcl  13742  subgsubcl  13743  subgsub  13744  subgmulg  13746  nsgconj  13764  nsgid  13773  quseccl0g  13789  ghmmulg  13814  ghmeqker  13829  f1ghm0to0  13830  kerf1ghm  13832  ablinvadd  13868  ablsub4  13871  ablpncan2  13874  subgabl  13890  gsumfzconst  13899  rngcl  13928  imasrng  13940  srgcl  13954  ringcl  13997  crngcom  13998  ringidss  14013  ringcom  14015  imasring  14048  opprringbg  14064  unitmulcl  14098  unitmulclb  14099  dvrcl  14120  unitdvcl  14121  dvrcan1  14125  dvrcan3  14126  rhmmul  14149  subrngrng  14187  subrngmcl  14194  subrgmcl  14218  subrgdv  14223  rrgeq0  14250  domneq0  14257  islmod  14276  scafvalg  14292  lmodcom  14318  rmodislmodlem  14335  rmodislmod  14336  lssclg  14349  lssvnegcl  14361  lssintclm  14369  lspss  14384  lspun  14387  lspsnvsi  14403  rspssp  14479  rnglidlmmgm  14481  rnglidlmsgrp  14482  rnglidlrng  14483  zndvds  14634  2basgeng  14777  iuncld  14810  ntrss  14814  restco  14869  restabs  14870  cnprcl2k  14901  lmconst  14911  cnrest2  14931  cnmpt2t  14988  psmetsym  15024  psmetge0  15026  xmetge0  15060  xmetsym  15063  blvalps  15083  blval  15084  xblcntrps  15108  xblcntr  15109  xmssym  15164  blsscls2  15188  bdxmet  15196  txmetcnp  15213  dvfvalap  15376  dvid  15390  dvidre  15392  dvcnp2cntop  15394  elplyr  15435  rpcxpadd  15600  rpcxpsub  15603  rpmulcxp  15604  rpdivcxp  15606  cxpmul  15607  rpcxple2  15613  rpcxplt2  15614  rplogbval  15640  rplogbcl  15641  rplogbreexp  15648  relogbexpap  15653  logbleb  15656  logblt  15657  rplogbcxp  15658  rpcxplogb  15659  relogbcxpbap  15660  sgmppw  15687  lgsneg1  15725  lgsmod  15726  lgsne0  15738  lgssq  15740  lgsdirnn0  15747  lgsdinn0  15748  lgsquad  15780  funvtxvalg  15858  funiedgvalg  15859  lpvtx  15900  ausgrumgrien  15989  ausgrusgrien  15990  wlkl1loop  16130  findset  16417