Theorem simp2 1000

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

Syntax hints:   → wi 4   ∧ w3a 980

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 982

This theorem is referenced by:  simpl2  1003  simpr2  1006  simp2i  1009  simp2d  1012  simp12  1030  simp22  1033  simp32  1036  syld3an3  1294  3ianorr  1320  stoic4b  1444  nlim0  4430  tfisi  4624  sotri2  5068  sotri3  5069  feq123  5402  sefvex  5582  fvmptt  5656  fnfvima  5800  cocan1  5837  cocan2  5838  ovexg  5959  ovmpox  6055  ovmpoga  6056  fvmpopr2d  6063  caovimo  6121  tfr1onlembxssdm  6410  tfr1onlembfn  6411  tfrcllembxssdm  6423  tfrcllembfn  6424  freccllem  6469  frecfcllem  6471  frecsuclem  6473  frecrdg  6475  mapxpen  6918  dif1en  6949  diffifi  6964  unsnfidcex  6990  unfidisj  6992  undifdc  6994  resfnfinfinss  7014  funrnfi  7017  sbthlemi9  7040  elfir  7048  difinfsn  7175  ctssdc  7188  djuassen  7300  xpdjuen  7301  mulcanenq  7469  ltanqg  7484  mulcanenq0ec  7529  addnnnq0  7533  distrprg  7672  aptipr  7725  addsrpr  7829  mulsrpr  7830  mulasssrg  7842  ltpsrprg  7887  axmulass  7957  axpre-ltadd  7970  subadd2  8247  nppcan  8265  nppcan3  8267  subsub2  8271  subsub4  8276  npncan3  8281  pnpcan  8282  pnncan  8284  subcan  8298  ltadd1  8473  leadd1  8474  leadd2  8475  ltsubadd  8476  ltsubadd2  8477  lesubadd  8478  lesubadd2  8479  ltaddsub  8480  leaddsub  8482  lesub1  8500  lesub2  8501  ltsub1  8502  ltsub2  8503  gt0add  8617  apreap  8631  lemul1  8637  reapmul1lem  8638  reapmul1  8639  reapadd1  8640  remulext1  8643  remulext2  8644  apadd2  8653  mulext2  8657  mulap0r  8659  leltap  8669  ltap  8677  apsub1  8686  recexaplem2  8696  mulcanap  8709  mulcanap2  8710  divvalap  8718  divmulap  8719  divcanap1  8725  diveqap0  8726  divap0b  8727  divrecap  8732  divassap  8734  div23ap  8735  divdirap  8741  divcanap3  8742  div11ap  8744  diveqap1  8749  divmuldivap  8756  divcanap5  8758  redivclap  8775  div2negap  8779  apmul1  8832  apmul2  8833  div2subap  8881  ltdiv1  8912  ledivmul  8921  lemuldiv  8925  lt2msq1  8929  ltdiv23  8936  squeeze0  8948  ofnegsub  9006  zaddcllemneg  9382  eluzsub  9648  nn01to3  9708  rpgecl  9774  addlelt  9860  xleadd1  9967  xltadd1  9968  lbioog  10005  ubioc1  10021  ubicc2  10077  icoshftf1o  10083  fzen  10135  nelfzo  10244  ubmelfzo  10293  ssfzo12  10317  ubmelm1fzo  10319  fzosplitprm1  10327  zsupssdc  10345  rebtwn2zlemshrink  10360  qbtwnre  10363  icogelb  10372  flqwordi  10395  flqword2  10396  flltdivnn0lt  10411  modqcl  10435  mulqmod0  10439  modqmulnn  10451  modqabs2  10467  modqmuladdnn0  10477  qnegmod  10478  addmodid  10481  modqm1p1mod0  10484  modifeq2int  10495  modqdi  10501  modqeqmodmin  10503  modfzo0difsn  10504  frec2uzf1od  10515  exp3val  10650  expnegap0  10656  expgt1  10686  exprecap  10689  expmulzap  10694  leexp2a  10701  expubnd  10705  mulbinom2  10765  bernneq2  10770  expnbnd  10772  fihashss  10925  fihashssdif  10927  fimaxq  10936  shftuz  10999  shftfibg  11002  cjdivap  11091  resqrtcl  11211  absdivap  11252  abssubne0  11273  maxleast  11395  lemininf  11416  ltmininf  11417  xrmaxltsup  11440  xrmaxaddlem  11442  xrmaxadd  11443  xrmineqinf  11451  xrltmininf  11452  xrminltinf  11454  xrminadd  11457  climuni  11475  reccn2ap  11495  isumz  11571  geoisum1c  11702  prod1dc  11768  efltim  11880  dvdsval2  11972  dvdscmulr  12002  dvdsmulcr  12003  modmulconst  12005  dvdsadd2b  12022  dvdsexp  12043  mulmoddvds  12045  divalglemeuneg  12105  gcdaddm  12176  dvdsgcdb  12205  mulgcd  12208  gcddiv  12211  uzwodc  12229  lcmdvdsb  12277  mulgcddvds  12287  qredeq  12289  divgcdcoprm0  12294  cncongr1  12296  euclemma  12339  rpexp  12346  rpexp12i  12348  fermltl  12427  prmdiv  12428  odzcllem  12436  odzdvds  12439  odzphi  12440  vfermltl  12445  coprimeprodsq  12451  pythagtriplem6  12464  pythagtriplem7  12465  pythagtriplem12  12469  pythagtriplem13  12470  pceu  12489  pcdvdsb  12514  pcgcd1  12522  dvdsprmpweq  12529  sumhashdc  12541  ctinf  12672  fvsetsid  12737  ressressg  12778  ressabsg  12779  rngplusgg  12839  imasaddvallemg  13017  qusaddvallemg  13035  plusfvalg  13065  mgmb1mgm1  13070  issubmnd  13144  ress0g  13145  imasmnd2  13154  imasmnd  13155  gsumfzz  13197  grpasscan2  13266  grpidrcan  13267  grpidlcan  13268  grpinvadd  13280  grpsubeq0  13288  grppncan  13293  dfgrp3mlem  13300  dfgrp3me  13302  grpsubpropd2  13307  pwsinvg  13314  imasgrp2  13316  imasgrp  13317  mhmmnd  13322  mulgnn0p1  13339  mulgnnsubcl  13340  mulgnn0subcl  13341  mulgsubcl  13342  mulgneg  13346  mulgaddcom  13352  mulginvcom  13353  submmulg  13372  subgcl  13390  subgsubcl  13391  subgsub  13392  subgmulg  13394  nsgconj  13412  nsgid  13421  quseccl0g  13437  ghmmulg  13462  ghmeqker  13477  f1ghm0to0  13478  kerf1ghm  13480  ablinvadd  13516  ablsub4  13519  ablpncan2  13522  subgabl  13538  gsumfzconst  13547  rngcl  13576  imasrng  13588  srgcl  13602  ringcl  13645  crngcom  13646  ringidss  13661  ringcom  13663  imasring  13696  opprringbg  13712  unitmulcl  13745  unitmulclb  13746  dvrcl  13767  unitdvcl  13768  dvrcan1  13772  dvrcan3  13773  rhmmul  13796  subrngrng  13834  subrngmcl  13841  subrgmcl  13865  subrgdv  13870  rrgeq0  13897  domneq0  13904  islmod  13923  scafvalg  13939  lmodcom  13965  rmodislmodlem  13982  rmodislmod  13983  lssclg  13996  lssvnegcl  14008  lssintclm  14016  lspss  14031  lspun  14034  lspsnvsi  14050  rspssp  14126  rnglidlmmgm  14128  rnglidlmsgrp  14129  rnglidlrng  14130  zndvds  14281  2basgeng  14402  iuncld  14435  ntrss  14439  restco  14494  restabs  14495  cnprcl2k  14526  lmconst  14536  cnrest2  14556  cnmpt2t  14613  psmetsym  14649  psmetge0  14651  xmetge0  14685  xmetsym  14688  blvalps  14708  blval  14709  xblcntrps  14733  xblcntr  14734  xmssym  14789  blsscls2  14813  bdxmet  14821  txmetcnp  14838  dvfvalap  15001  dvid  15015  dvidre  15017  dvcnp2cntop  15019  elplyr  15060  rpcxpadd  15225  rpcxpsub  15228  rpmulcxp  15229  rpdivcxp  15231  cxpmul  15232  rpcxple2  15238  rpcxplt2  15239  rplogbval  15265  rplogbcl  15266  rplogbreexp  15273  relogbexpap  15278  logbleb  15281  logblt  15282  rplogbcxp  15283  rpcxplogb  15284  relogbcxpbap  15285  sgmppw  15312  lgsneg1  15350  lgsmod  15351  lgsne0  15363  lgssq  15365  lgsdirnn0  15372  lgsdinn0  15373  lgsquad  15405  findset  15675