Theorem simp2 988

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

Syntax hints:   → wi 4   ∧ w3a 968

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106

This theorem depends on definitions:  df-bi 116  df-3an 970

This theorem is referenced by:  simpl2  991  simpr2  994  simp2i  997  simp2d  1000  simp12  1018  simp22  1021  simp32  1024  syld3an3  1273  3ianorr  1299  stoic4b  1421  nlim0  4371  tfisi  4563  sotri2  5000  sotri3  5001  feq123  5328  sefvex  5506  fvmptt  5576  fnfvima  5718  cocan1  5754  cocan2  5755  ovexg  5872  ovmpox  5966  ovmpoga  5967  caovimo  6031  tfr1onlembxssdm  6307  tfr1onlembfn  6308  tfrcllembxssdm  6320  tfrcllembfn  6321  freccllem  6366  frecfcllem  6368  frecsuclem  6370  frecrdg  6372  mapxpen  6810  dif1en  6841  diffifi  6856  unsnfidcex  6881  unfidisj  6883  undifdc  6885  resfnfinfinss  6901  funrnfi  6903  sbthlemi9  6926  elfir  6934  difinfsn  7061  ctssdc  7074  djuassen  7169  xpdjuen  7170  mulcanenq  7322  ltanqg  7337  mulcanenq0ec  7382  addnnnq0  7386  distrprg  7525  aptipr  7578  addsrpr  7682  mulsrpr  7683  mulasssrg  7695  ltpsrprg  7740  axmulass  7810  axpre-ltadd  7823  subadd2  8098  nppcan  8116  nppcan3  8118  subsub2  8122  subsub4  8127  npncan3  8132  pnpcan  8133  pnncan  8135  subcan  8149  ltadd1  8323  leadd1  8324  leadd2  8325  ltsubadd  8326  ltsubadd2  8327  lesubadd  8328  lesubadd2  8329  ltaddsub  8330  leaddsub  8332  lesub1  8350  lesub2  8351  ltsub1  8352  ltsub2  8353  gt0add  8467  apreap  8481  lemul1  8487  reapmul1lem  8488  reapmul1  8489  reapadd1  8490  remulext1  8493  remulext2  8494  apadd2  8503  mulext2  8507  mulap0r  8509  leltap  8519  ltap  8527  apsub1  8536  recexaplem2  8545  mulcanap  8558  mulcanap2  8559  divvalap  8566  divmulap  8567  divcanap1  8573  diveqap0  8574  divap0b  8575  divrecap  8580  divassap  8582  div23ap  8583  divdirap  8589  divcanap3  8590  div11ap  8592  diveqap1  8597  divmuldivap  8604  divcanap5  8606  redivclap  8623  div2negap  8627  apmul1  8680  apmul2  8681  div2subap  8729  ltdiv1  8759  ledivmul  8768  lemuldiv  8772  lt2msq1  8776  ltdiv23  8783  squeeze0  8795  zaddcllemneg  9226  eluzsub  9491  nn01to3  9551  rpgecl  9614  addlelt  9700  xleadd1  9807  xltadd1  9808  lbioog  9845  ubioc1  9861  ubicc2  9917  icoshftf1o  9923  fzen  9974  ubmelfzo  10131  ssfzo12  10155  ubmelm1fzo  10157  fzosplitprm1  10165  rebtwn2zlemshrink  10185  qbtwnre  10188  icogelb  10197  flqwordi  10219  flqword2  10220  flltdivnn0lt  10235  modqcl  10257  mulqmod0  10261  modqmulnn  10273  modqabs2  10289  modqmuladdnn0  10299  qnegmod  10300  addmodid  10303  modqm1p1mod0  10306  modifeq2int  10317  modqdi  10323  modqeqmodmin  10325  modfzo0difsn  10326  frec2uzf1od  10337  exp3val  10453  expnegap0  10459  expgt1  10489  exprecap  10492  expmulzap  10497  leexp2a  10504  expubnd  10508  mulbinom2  10567  bernneq2  10572  expnbnd  10574  fihashss  10725  fihashssdif  10727  fimaxq  10736  shftuz  10755  shftfibg  10758  cjdivap  10847  resqrtcl  10967  absdivap  11008  abssubne0  11029  maxleast  11151  lemininf  11171  ltmininf  11172  xrmaxltsup  11195  xrmaxaddlem  11197  xrmaxadd  11198  xrmineqinf  11206  xrltmininf  11207  xrminltinf  11209  xrminadd  11212  climuni  11230  reccn2ap  11250  isumz  11326  geoisum1c  11457  prod1dc  11523  efltim  11635  dvdsval2  11726  dvdscmulr  11756  dvdsmulcr  11757  modmulconst  11759  dvdsadd2b  11776  dvdsexp  11795  mulmoddvds  11797  divalglemeuneg  11856  zsupssdc  11883  gcdaddm  11913  dvdsgcdb  11942  mulgcd  11945  gcddiv  11948  uzwodc  11966  lcmdvdsb  12012  mulgcddvds  12022  qredeq  12024  divgcdcoprm0  12029  cncongr1  12031  euclemma  12074  rpexp  12081  rpexp12i  12083  fermltl  12162  prmdiv  12163  odzcllem  12170  odzdvds  12173  odzphi  12174  vfermltl  12179  coprimeprodsq  12185  pythagtriplem6  12198  pythagtriplem7  12199  pythagtriplem12  12203  pythagtriplem13  12204  pceu  12223  pcdvdsb  12247  pcgcd1  12255  dvdsprmpweq  12262  sumhashdc  12273  ctinf  12359  fvsetsid  12424  ressid2  12449  ressval2  12450  rngplusgg  12507  2basgeng  12682  iuncld  12715  ntrss  12719  restco  12774  restabs  12775  cnprcl2k  12806  lmconst  12816  cnrest2  12836  cnmpt2t  12893  psmetsym  12929  psmetge0  12931  xmetge0  12965  xmetsym  12968  blvalps  12988  blval  12989  xblcntrps  13013  xblcntr  13014  xmssym  13069  blsscls2  13093  bdxmet  13101  txmetcnp  13118  dvfvalap  13250  dvid  13262  dvcnp2cntop  13263  rpcxpadd  13426  rpcxpsub  13429  rpmulcxp  13430  rpdivcxp  13432  cxpmul  13433  rpcxple2  13438  rpcxplt2  13439  rplogbval  13463  rplogbcl  13464  rplogbreexp  13471  relogbexpap  13476  logbleb  13479  logblt  13480  rplogbcxp  13481  rpcxplogb  13482  relogbcxpbap  13483  lgsneg1  13526  lgsmod  13527  lgsne0  13539  lgssq  13541  lgsdirnn0  13548  lgsdinn0  13549  findset  13787