Theorem simp2 1025

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

Syntax hints:   → wi 4   ∧ w3a 1005

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 1007

This theorem is referenced by:  simpl2  1028  simpr2  1031  simp2i  1034  simp2d  1037  simp12  1055  simp22  1058  simp32  1061  syld3an3  1319  3ianorr  1346  intn3an2d  1394  stoic4b  1478  nlim0  4520  tfisi  4714  sotri2  5165  sotri3  5166  feq123  5505  sefvex  5696  fvmptt  5774  fnfvima  5926  cocan1  5966  cocan2  5967  ovexg  6092  ovmpox  6190  ovmpoga  6191  fvmpopr2d  6198  caovimo  6256  suppval1  6452  suppimacnvfn  6459  suppfnss  6470  tfr1onlembxssdm  6587  tfr1onlembfn  6588  tfrcllembxssdm  6600  tfrcllembfn  6601  freccllem  6646  frecfcllem  6648  frecsuclem  6650  frecrdg  6652  domssr  7030  mapxpen  7114  dif1en  7149  diffifi  7164  unsnfidcex  7193  unfidisj  7195  undifdc  7197  resfnfinfinss  7219  funrnfi  7222  fissfi  7229  sbthlemi9  7248  elfir  7273  difinfsn  7404  ctssdc  7417  djuassen  7537  xpdjuen  7538  mulcanenq  7716  ltanqg  7731  mulcanenq0ec  7776  addnnnq0  7780  distrprg  7919  aptipr  7972  addsrpr  8076  mulsrpr  8077  mulasssrg  8089  ltpsrprg  8134  axmulass  8204  axpre-ltadd  8217  subadd2  8494  nppcan  8512  nppcan3  8514  subsub2  8518  subsub4  8523  npncan3  8528  pnpcan  8529  pnncan  8531  subcan  8545  ltadd1  8721  leadd1  8722  leadd2  8723  ltsubadd  8724  ltsubadd2  8725  lesubadd  8726  lesubadd2  8727  ltaddsub  8728  leaddsub  8730  lesub1  8748  lesub2  8749  ltsub1  8750  ltsub2  8751  gt0add  8865  apreap  8879  lemul1  8885  reapmul1lem  8886  reapmul1  8887  reapadd1  8888  remulext1  8891  remulext2  8892  apadd2  8901  mulext2  8905  mulap0r  8907  leltap  8917  ltap  8925  apsub1  8934  recexaplem2  8944  mulcanap  8957  mulcanap2  8958  divvalap  8968  divmulap  8969  divcanap1  8975  diveqap0  8976  divap0b  8977  divrecap  8982  divassap  8984  div23ap  8985  divdirap  8991  divcanap3  8992  div11ap  8994  diveqap1  8999  divmuldivap  9006  divcanap5  9008  redivclap  9025  div2negap  9029  apmul1  9082  apmul2  9083  div2subap  9131  ltdiv1  9162  ledivmul  9171  lemuldiv  9175  lt2msq1  9179  ltdiv23  9186  squeeze0  9198  ofnegsub  9256  zaddcllemneg  9636  zfidc  9676  eluzsub  9905  nn01to3  9970  rpgecl  10036  addlelt  10122  xleadd1  10230  xltadd1  10231  lbioog  10268  ubioc1  10284  ubicc2  10340  icoshftf1o  10346  fzen  10400  nelfzo  10511  ubmelfzo  10570  ssfzo12  10594  ubmelm1fzo  10596  fzosplitprm1  10605  zsupssdc  10625  rebtwn2zlemshrink  10640  qbtwnre  10643  icogelb  10652  flqwordi  10675  flqword2  10676  flltdivnn0lt  10691  modqcl  10715  mulqmod0  10719  modqmulnn  10731  modqabs2  10747  modqmuladdnn0  10757  qnegmod  10758  addmodid  10761  modqm1p1mod0  10764  modifeq2int  10775  modqdi  10781  modqeqmodmin  10783  modfzo0difsn  10784  frec2uzf1od  10795  exp3val  10930  expnegap0  10936  expgt1  10966  exprecap  10969  expmulzap  10974  leexp2a  10981  expubnd  10985  mulbinom2  11045  bernneq2  11051  expnbnd  11053  fihashss  11209  fihashssdif  11211  fimaxq  11222  ccatval2  11314  ccatass  11324  ccatw2s1leng  11354  ccat2s1fvwd  11363  swrdval  11368  swrdnd  11379  pfxfv  11404  pfxpfx  11428  ccats1pfxeq  11434  ccats1pfxeqrex  11435  s3cl  11506  s3fv0g  11511  s3fv1g  11512  s3fv2g  11513  shftuz  11530  shftfibg  11533  cjdivap  11622  resqrtcl  11742  absdivap  11783  abssubne0  11804  maxleast  11926  lemininf  11947  ltmininf  11948  xrmaxltsup  11971  xrmaxaddlem  11973  xrmaxadd  11974  xrmineqinf  11982  xrltmininf  11983  xrminltinf  11985  xrminadd  11988  climuni  12006  reccn2ap  12026  isumz  12103  geoisum1c  12234  prod1dc  12300  efltim  12412  dvdsval2  12504  dvdscmulr  12534  dvdsmulcr  12535  modmulconst  12537  dvdsadd2b  12554  dvdsexp  12575  mulmoddvds  12577  divalglemeuneg  12637  gcdaddm  12708  dvdsgcdb  12737  mulgcd  12740  gcddiv  12743  uzwodc  12761  lcmdvdsb  12809  mulgcddvds  12819  qredeq  12821  divgcdcoprm0  12826  cncongr1  12828  euclemma  12871  rpexp  12878  rpexp12i  12880  fermltl  12959  prmdiv  12960  odzcllem  12968  odzdvds  12971  odzphi  12972  vfermltl  12977  coprimeprodsq  12983  pythagtriplem6  12996  pythagtriplem7  12997  pythagtriplem12  13001  pythagtriplem13  13002  pceu  13021  pcdvdsb  13046  pcgcd1  13054  dvdsprmpweq  13061  sumhashdc  13073  ctinf  13268  fvsetsid  13333  ressressg  13375  ressabsg  13376  rngplusgg  13437  imasaddvallemg  13582  qusaddvallemg  13600  plusfvalg  13629  mgmb1mgm1  13634  issubmnd  13706  ress0g  13707  imasmnd2  13710  imasmnd  13711  gsumfzz  13753  grpasscan2  13822  grpidrcan  13823  grpidlcan  13824  grpinvadd  13836  grpsubeq0  13844  grppncan  13849  dfgrp3mlem  13856  dfgrp3me  13858  grpsubpropd2  13863  imasgrp2  13866  imasgrp  13867  mhmmnd  13872  mulgnn0p1  13889  mulgnnsubcl  13890  mulgnn0subcl  13891  mulgsubcl  13892  mulgneg  13896  mulgaddcom  13902  mulginvcom  13903  submmulg  13922  subgcl  13940  subgsubcl  13941  subgsub  13942  subgmulg  13944  nsgconj  13962  nsgid  13971  quseccl0g  13987  ghmmulg  14012  ghmeqker  14027  f1ghm0to0  14028  kerf1ghm  14030  ablinvadd  14066  ablsub4  14069  ablpncan2  14072  subgabl  14088  gsumfzconst  14097  gfsumsn  14110  pwsinvg  14160  rngcl  14186  imasrng  14198  srgcl  14216  ringcl  14259  crngcom  14260  ringidss  14275  ringcom  14277  imasring  14310  opprringbg  14326  unitmulcl  14361  unitmulclb  14362  dvrcl  14383  unitdvcl  14384  dvrcan1  14388  dvrcan3  14389  rhmmul  14412  subrngrng  14451  subrngmcl  14458  subrgmcl  14482  subrgdv  14487  rrgeq0  14514  domneq0  14522  islmod  14568  scafvalg  14584  lmodcom  14610  rmodislmodlem  14627  rmodislmod  14628  lssclg  14641  lssvnegcl  14653  lssintclm  14661  lspss  14676  lspun  14679  lspsnvsi  14695  rspssp  14771  rnglidlmmgm  14773  rnglidlmsgrp  14774  rnglidlrng  14775  zndvds  14926  psrbaglecl  14953  psrbagcon  14955  2basgeng  15076  iuncld  15109  ntrss  15113  restco  15168  restabs  15169  cnprcl2k  15200  lmconst  15210  cnrest2  15230  cnmpt2t  15287  psmetsym  15323  psmetge0  15325  xmetge0  15359  xmetsym  15362  blvalps  15382  blval  15383  xblcntrps  15407  xblcntr  15408  xmssym  15463  blsscls2  15487  bdxmet  15495  txmetcnp  15512  dvfvalap  15675  dvid  15689  dvidre  15691  dvcnp2cntop  15693  elplyr  15734  rpcxpadd  15899  rpcxpsub  15902  rpmulcxp  15903  rpdivcxp  15905  cxpmul  15906  rpcxple2  15912  rpcxplt2  15913  rplogbval  15939  rplogbcl  15940  rplogbreexp  15947  relogbexpap  15952  logbleb  15955  logblt  15956  rplogbcxp  15957  rpcxplogb  15958  relogbcxpbap  15959  sgmppw  15989  lgsneg1  16027  lgsmod  16028  lgsne0  16040  lgssq  16042  lgsdirnn0  16049  lgsdinn0  16050  lgsquad  16082  funvtxvalg  16160  funiedgvalg  16161  lpvtx  16203  ausgrumgrien  16294  ausgrusgrien  16295  uhgrissubgr  16385  egrsubgr  16387  subumgredg2en  16395  subusgr  16399  wlkl1loop  16482  clwwlknonex2  16563  eulerpathprum  16604  eulerpathum  16605  findset  16854  repiecele0  16949  repiecege0  16950