Theorem simp2 998

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

Syntax hints:   → wi 4   ∧ w3a 978

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 980

This theorem is referenced by:  simpl2  1001  simpr2  1004  simp2i  1007  simp2d  1010  simp12  1028  simp22  1031  simp32  1034  syld3an3  1283  3ianorr  1309  stoic4b  1431  nlim0  4388  tfisi  4580  sotri2  5018  sotri3  5019  feq123  5349  sefvex  5528  fvmptt  5599  fnfvima  5742  cocan1  5778  cocan2  5779  ovexg  5899  ovmpox  5993  ovmpoga  5994  caovimo  6058  tfr1onlembxssdm  6334  tfr1onlembfn  6335  tfrcllembxssdm  6347  tfrcllembfn  6348  freccllem  6393  frecfcllem  6395  frecsuclem  6397  frecrdg  6399  mapxpen  6838  dif1en  6869  diffifi  6884  unsnfidcex  6909  unfidisj  6911  undifdc  6913  resfnfinfinss  6929  funrnfi  6931  sbthlemi9  6954  elfir  6962  difinfsn  7089  ctssdc  7102  djuassen  7206  xpdjuen  7207  mulcanenq  7359  ltanqg  7374  mulcanenq0ec  7419  addnnnq0  7423  distrprg  7562  aptipr  7615  addsrpr  7719  mulsrpr  7720  mulasssrg  7732  ltpsrprg  7777  axmulass  7847  axpre-ltadd  7860  subadd2  8135  nppcan  8153  nppcan3  8155  subsub2  8159  subsub4  8164  npncan3  8169  pnpcan  8170  pnncan  8172  subcan  8186  ltadd1  8360  leadd1  8361  leadd2  8362  ltsubadd  8363  ltsubadd2  8364  lesubadd  8365  lesubadd2  8366  ltaddsub  8367  leaddsub  8369  lesub1  8387  lesub2  8388  ltsub1  8389  ltsub2  8390  gt0add  8504  apreap  8518  lemul1  8524  reapmul1lem  8525  reapmul1  8526  reapadd1  8527  remulext1  8530  remulext2  8531  apadd2  8540  mulext2  8544  mulap0r  8546  leltap  8556  ltap  8564  apsub1  8573  recexaplem2  8582  mulcanap  8595  mulcanap2  8596  divvalap  8603  divmulap  8604  divcanap1  8610  diveqap0  8611  divap0b  8612  divrecap  8617  divassap  8619  div23ap  8620  divdirap  8626  divcanap3  8627  div11ap  8629  diveqap1  8634  divmuldivap  8641  divcanap5  8643  redivclap  8660  div2negap  8664  apmul1  8717  apmul2  8718  div2subap  8766  ltdiv1  8796  ledivmul  8805  lemuldiv  8809  lt2msq1  8813  ltdiv23  8820  squeeze0  8832  zaddcllemneg  9263  eluzsub  9528  nn01to3  9588  rpgecl  9651  addlelt  9737  xleadd1  9844  xltadd1  9845  lbioog  9882  ubioc1  9898  ubicc2  9954  icoshftf1o  9960  fzen  10011  ubmelfzo  10168  ssfzo12  10192  ubmelm1fzo  10194  fzosplitprm1  10202  rebtwn2zlemshrink  10222  qbtwnre  10225  icogelb  10234  flqwordi  10256  flqword2  10257  flltdivnn0lt  10272  modqcl  10294  mulqmod0  10298  modqmulnn  10310  modqabs2  10326  modqmuladdnn0  10336  qnegmod  10337  addmodid  10340  modqm1p1mod0  10343  modifeq2int  10354  modqdi  10360  modqeqmodmin  10362  modfzo0difsn  10363  frec2uzf1od  10374  exp3val  10490  expnegap0  10496  expgt1  10526  exprecap  10529  expmulzap  10534  leexp2a  10541  expubnd  10545  mulbinom2  10604  bernneq2  10609  expnbnd  10611  fihashss  10762  fihashssdif  10764  fimaxq  10773  shftuz  10792  shftfibg  10795  cjdivap  10884  resqrtcl  11004  absdivap  11045  abssubne0  11066  maxleast  11188  lemininf  11208  ltmininf  11209  xrmaxltsup  11232  xrmaxaddlem  11234  xrmaxadd  11235  xrmineqinf  11243  xrltmininf  11244  xrminltinf  11246  xrminadd  11249  climuni  11267  reccn2ap  11287  isumz  11363  geoisum1c  11494  prod1dc  11560  efltim  11672  dvdsval2  11763  dvdscmulr  11793  dvdsmulcr  11794  modmulconst  11796  dvdsadd2b  11813  dvdsexp  11832  mulmoddvds  11834  divalglemeuneg  11893  zsupssdc  11920  gcdaddm  11950  dvdsgcdb  11979  mulgcd  11982  gcddiv  11985  uzwodc  12003  lcmdvdsb  12049  mulgcddvds  12059  qredeq  12061  divgcdcoprm0  12066  cncongr1  12068  euclemma  12111  rpexp  12118  rpexp12i  12120  fermltl  12199  prmdiv  12200  odzcllem  12207  odzdvds  12210  odzphi  12211  vfermltl  12216  coprimeprodsq  12222  pythagtriplem6  12235  pythagtriplem7  12236  pythagtriplem12  12240  pythagtriplem13  12241  pceu  12260  pcdvdsb  12284  pcgcd1  12292  dvdsprmpweq  12299  sumhashdc  12310  ctinf  12396  fvsetsid  12461  ressid2  12488  ressval2  12489  rngplusgg  12546  plusfvalg  12646  mgmb1mgm1  12651  grpasscan2  12793  grpidrcan  12794  grpidlcan  12795  grpinvadd  12807  grpsubeq0  12815  grppncan  12820  dfgrp3mlem  12827  dfgrp3me  12829  grpsubpropd2  12834  mhmmnd  12839  mulgnn0p1  12853  mulgnnsubcl  12854  mulgnn0subcl  12855  mulgsubcl  12856  mulgneg  12860  mulgaddcom  12865  mulginvcom  12866  ablinvadd  12910  ablsub4  12913  ablpncan2  12916  srgcl  12948  ringcl  12991  crngcom  12992  ringcom  13008  opprringbg  13043  2basgeng  13151  iuncld  13184  ntrss  13188  restco  13243  restabs  13244  cnprcl2k  13275  lmconst  13285  cnrest2  13305  cnmpt2t  13362  psmetsym  13398  psmetge0  13400  xmetge0  13434  xmetsym  13437  blvalps  13457  blval  13458  xblcntrps  13482  xblcntr  13483  xmssym  13538  blsscls2  13562  bdxmet  13570  txmetcnp  13587  dvfvalap  13719  dvid  13731  dvcnp2cntop  13732  rpcxpadd  13895  rpcxpsub  13898  rpmulcxp  13899  rpdivcxp  13901  cxpmul  13902  rpcxple2  13907  rpcxplt2  13908  rplogbval  13932  rplogbcl  13933  rplogbreexp  13940  relogbexpap  13945  logbleb  13948  logblt  13949  rplogbcxp  13950  rpcxplogb  13951  relogbcxpbap  13952  lgsneg1  13995  lgsmod  13996  lgsne0  14008  lgssq  14010  lgsdirnn0  14017  lgsdinn0  14018  findset  14255