Theorem simp2 1003

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 999	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜑 ∧ 𝜓))
2	1	simprd 114	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓)

Syntax hints:   → wi 4   ∧ w3a 983

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 985

This theorem is referenced by:  simpl2  1006  simpr2  1009  simp2i  1012  simp2d  1015  simp12  1033  simp22  1036  simp32  1039  syld3an3  1297  3ianorr  1324  intn3an2d  1371  stoic4b  1455  nlim0  4462  tfisi  4656  sotri2  5102  sotri3  5103  feq123  5441  sefvex  5624  fvmptt  5699  fnfvima  5847  cocan1  5884  cocan2  5885  ovexg  6008  ovmpox  6104  ovmpoga  6105  fvmpopr2d  6112  caovimo  6170  tfr1onlembxssdm  6459  tfr1onlembfn  6460  tfrcllembxssdm  6472  tfrcllembfn  6473  freccllem  6518  frecfcllem  6520  frecsuclem  6522  frecrdg  6524  domssr  6899  mapxpen  6977  dif1en  7009  diffifi  7024  unsnfidcex  7050  unfidisj  7052  undifdc  7054  resfnfinfinss  7074  funrnfi  7077  sbthlemi9  7100  elfir  7108  difinfsn  7235  ctssdc  7248  djuassen  7367  xpdjuen  7368  mulcanenq  7540  ltanqg  7555  mulcanenq0ec  7600  addnnnq0  7604  distrprg  7743  aptipr  7796  addsrpr  7900  mulsrpr  7901  mulasssrg  7913  ltpsrprg  7958  axmulass  8028  axpre-ltadd  8041  subadd2  8318  nppcan  8336  nppcan3  8338  subsub2  8342  subsub4  8347  npncan3  8352  pnpcan  8353  pnncan  8355  subcan  8369  ltadd1  8544  leadd1  8545  leadd2  8546  ltsubadd  8547  ltsubadd2  8548  lesubadd  8549  lesubadd2  8550  ltaddsub  8551  leaddsub  8553  lesub1  8571  lesub2  8572  ltsub1  8573  ltsub2  8574  gt0add  8688  apreap  8702  lemul1  8708  reapmul1lem  8709  reapmul1  8710  reapadd1  8711  remulext1  8714  remulext2  8715  apadd2  8724  mulext2  8728  mulap0r  8730  leltap  8740  ltap  8748  apsub1  8757  recexaplem2  8767  mulcanap  8780  mulcanap2  8781  divvalap  8789  divmulap  8790  divcanap1  8796  diveqap0  8797  divap0b  8798  divrecap  8803  divassap  8805  div23ap  8806  divdirap  8812  divcanap3  8813  div11ap  8815  diveqap1  8820  divmuldivap  8827  divcanap5  8829  redivclap  8846  div2negap  8850  apmul1  8903  apmul2  8904  div2subap  8952  ltdiv1  8983  ledivmul  8992  lemuldiv  8996  lt2msq1  9000  ltdiv23  9007  squeeze0  9019  ofnegsub  9077  zaddcllemneg  9453  eluzsub  9720  nn01to3  9780  rpgecl  9846  addlelt  9932  xleadd1  10039  xltadd1  10040  lbioog  10077  ubioc1  10093  ubicc2  10149  icoshftf1o  10155  fzen  10207  nelfzo  10316  ubmelfzo  10373  ssfzo12  10397  ubmelm1fzo  10399  fzosplitprm1  10407  zsupssdc  10425  rebtwn2zlemshrink  10440  qbtwnre  10443  icogelb  10452  flqwordi  10475  flqword2  10476  flltdivnn0lt  10491  modqcl  10515  mulqmod0  10519  modqmulnn  10531  modqabs2  10547  modqmuladdnn0  10557  qnegmod  10558  addmodid  10561  modqm1p1mod0  10564  modifeq2int  10575  modqdi  10581  modqeqmodmin  10583  modfzo0difsn  10584  frec2uzf1od  10595  exp3val  10730  expnegap0  10736  expgt1  10766  exprecap  10769  expmulzap  10774  leexp2a  10781  expubnd  10785  mulbinom2  10845  bernneq2  10850  expnbnd  10852  fihashss  11005  fihashssdif  11007  fimaxq  11016  ccatval2  11099  ccatass  11109  swrdval  11146  swrdnd  11157  pfxfv  11182  pfxpfx  11206  ccats1pfxeq  11212  ccats1pfxeqrex  11213  s3cl  11284  s3fv0g  11289  s3fv1g  11290  shftuz  11294  shftfibg  11297  cjdivap  11386  resqrtcl  11506  absdivap  11547  abssubne0  11568  maxleast  11690  lemininf  11711  ltmininf  11712  xrmaxltsup  11735  xrmaxaddlem  11737  xrmaxadd  11738  xrmineqinf  11746  xrltmininf  11747  xrminltinf  11749  xrminadd  11752  climuni  11770  reccn2ap  11790  isumz  11866  geoisum1c  11997  prod1dc  12063  efltim  12175  dvdsval2  12267  dvdscmulr  12297  dvdsmulcr  12298  modmulconst  12300  dvdsadd2b  12317  dvdsexp  12338  mulmoddvds  12340  divalglemeuneg  12400  gcdaddm  12471  dvdsgcdb  12500  mulgcd  12503  gcddiv  12506  uzwodc  12524  lcmdvdsb  12572  mulgcddvds  12582  qredeq  12584  divgcdcoprm0  12589  cncongr1  12591  euclemma  12634  rpexp  12641  rpexp12i  12643  fermltl  12722  prmdiv  12723  odzcllem  12731  odzdvds  12734  odzphi  12735  vfermltl  12740  coprimeprodsq  12746  pythagtriplem6  12759  pythagtriplem7  12760  pythagtriplem12  12764  pythagtriplem13  12765  pceu  12784  pcdvdsb  12809  pcgcd1  12817  dvdsprmpweq  12824  sumhashdc  12836  ctinf  12967  fvsetsid  13032  ressressg  13074  ressabsg  13075  rngplusgg  13136  imasaddvallemg  13314  qusaddvallemg  13332  plusfvalg  13362  mgmb1mgm1  13367  issubmnd  13441  ress0g  13442  imasmnd2  13451  imasmnd  13452  gsumfzz  13494  grpasscan2  13563  grpidrcan  13564  grpidlcan  13565  grpinvadd  13577  grpsubeq0  13585  grppncan  13590  dfgrp3mlem  13597  dfgrp3me  13599  grpsubpropd2  13604  pwsinvg  13611  imasgrp2  13613  imasgrp  13614  mhmmnd  13619  mulgnn0p1  13636  mulgnnsubcl  13637  mulgnn0subcl  13638  mulgsubcl  13639  mulgneg  13643  mulgaddcom  13649  mulginvcom  13650  submmulg  13669  subgcl  13687  subgsubcl  13688  subgsub  13689  subgmulg  13691  nsgconj  13709  nsgid  13718  quseccl0g  13734  ghmmulg  13759  ghmeqker  13774  f1ghm0to0  13775  kerf1ghm  13777  ablinvadd  13813  ablsub4  13816  ablpncan2  13819  subgabl  13835  gsumfzconst  13844  rngcl  13873  imasrng  13885  srgcl  13899  ringcl  13942  crngcom  13943  ringidss  13958  ringcom  13960  imasring  13993  opprringbg  14009  unitmulcl  14042  unitmulclb  14043  dvrcl  14064  unitdvcl  14065  dvrcan1  14069  dvrcan3  14070  rhmmul  14093  subrngrng  14131  subrngmcl  14138  subrgmcl  14162  subrgdv  14167  rrgeq0  14194  domneq0  14201  islmod  14220  scafvalg  14236  lmodcom  14262  rmodislmodlem  14279  rmodislmod  14280  lssclg  14293  lssvnegcl  14305  lssintclm  14313  lspss  14328  lspun  14331  lspsnvsi  14347  rspssp  14423  rnglidlmmgm  14425  rnglidlmsgrp  14426  rnglidlrng  14427  zndvds  14578  2basgeng  14721  iuncld  14754  ntrss  14758  restco  14813  restabs  14814  cnprcl2k  14845  lmconst  14855  cnrest2  14875  cnmpt2t  14932  psmetsym  14968  psmetge0  14970  xmetge0  15004  xmetsym  15007  blvalps  15027  blval  15028  xblcntrps  15052  xblcntr  15053  xmssym  15108  blsscls2  15132  bdxmet  15140  txmetcnp  15157  dvfvalap  15320  dvid  15334  dvidre  15336  dvcnp2cntop  15338  elplyr  15379  rpcxpadd  15544  rpcxpsub  15547  rpmulcxp  15548  rpdivcxp  15550  cxpmul  15551  rpcxple2  15557  rpcxplt2  15558  rplogbval  15584  rplogbcl  15585  rplogbreexp  15592  relogbexpap  15597  logbleb  15600  logblt  15601  rplogbcxp  15602  rpcxplogb  15603  relogbcxpbap  15604  sgmppw  15631  lgsneg1  15669  lgsmod  15670  lgsne0  15682  lgssq  15684  lgsdirnn0  15691  lgsdinn0  15692  lgsquad  15724  funvtxvalg  15802  funiedgvalg  15803  lpvtx  15844  ausgrumgrien  15933  ausgrusgrien  15934  findset  16218