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  1433  nlim0  4394  tfisi  4586  sotri2  5026  sotri3  5027  feq123  5357  sefvex  5536  fvmptt  5607  fnfvima  5751  cocan1  5787  cocan2  5788  ovexg  5908  ovmpox  6002  ovmpoga  6003  caovimo  6067  tfr1onlembxssdm  6343  tfr1onlembfn  6344  tfrcllembxssdm  6356  tfrcllembfn  6357  freccllem  6402  frecfcllem  6404  frecsuclem  6406  frecrdg  6408  mapxpen  6847  dif1en  6878  diffifi  6893  unsnfidcex  6918  unfidisj  6920  undifdc  6922  resfnfinfinss  6938  funrnfi  6940  sbthlemi9  6963  elfir  6971  difinfsn  7098  ctssdc  7111  djuassen  7215  xpdjuen  7216  mulcanenq  7383  ltanqg  7398  mulcanenq0ec  7443  addnnnq0  7447  distrprg  7586  aptipr  7639  addsrpr  7743  mulsrpr  7744  mulasssrg  7756  ltpsrprg  7801  axmulass  7871  axpre-ltadd  7884  subadd2  8160  nppcan  8178  nppcan3  8180  subsub2  8184  subsub4  8189  npncan3  8194  pnpcan  8195  pnncan  8197  subcan  8211  ltadd1  8385  leadd1  8386  leadd2  8387  ltsubadd  8388  ltsubadd2  8389  lesubadd  8390  lesubadd2  8391  ltaddsub  8392  leaddsub  8394  lesub1  8412  lesub2  8413  ltsub1  8414  ltsub2  8415  gt0add  8529  apreap  8543  lemul1  8549  reapmul1lem  8550  reapmul1  8551  reapadd1  8552  remulext1  8555  remulext2  8556  apadd2  8565  mulext2  8569  mulap0r  8571  leltap  8581  ltap  8589  apsub1  8598  recexaplem2  8608  mulcanap  8621  mulcanap2  8622  divvalap  8630  divmulap  8631  divcanap1  8637  diveqap0  8638  divap0b  8639  divrecap  8644  divassap  8646  div23ap  8647  divdirap  8653  divcanap3  8654  div11ap  8656  diveqap1  8661  divmuldivap  8668  divcanap5  8670  redivclap  8687  div2negap  8691  apmul1  8744  apmul2  8745  div2subap  8793  ltdiv1  8824  ledivmul  8833  lemuldiv  8837  lt2msq1  8841  ltdiv23  8848  squeeze0  8860  zaddcllemneg  9291  eluzsub  9556  nn01to3  9616  rpgecl  9681  addlelt  9767  xleadd1  9874  xltadd1  9875  lbioog  9912  ubioc1  9928  ubicc2  9984  icoshftf1o  9990  fzen  10042  ubmelfzo  10199  ssfzo12  10223  ubmelm1fzo  10225  fzosplitprm1  10233  rebtwn2zlemshrink  10253  qbtwnre  10256  icogelb  10265  flqwordi  10287  flqword2  10288  flltdivnn0lt  10303  modqcl  10325  mulqmod0  10329  modqmulnn  10341  modqabs2  10357  modqmuladdnn0  10367  qnegmod  10368  addmodid  10371  modqm1p1mod0  10374  modifeq2int  10385  modqdi  10391  modqeqmodmin  10393  modfzo0difsn  10394  frec2uzf1od  10405  exp3val  10521  expnegap0  10527  expgt1  10557  exprecap  10560  expmulzap  10565  leexp2a  10572  expubnd  10576  mulbinom2  10636  bernneq2  10641  expnbnd  10643  fihashss  10795  fihashssdif  10797  fimaxq  10806  shftuz  10825  shftfibg  10828  cjdivap  10917  resqrtcl  11037  absdivap  11078  abssubne0  11099  maxleast  11221  lemininf  11241  ltmininf  11242  xrmaxltsup  11265  xrmaxaddlem  11267  xrmaxadd  11268  xrmineqinf  11276  xrltmininf  11277  xrminltinf  11279  xrminadd  11282  climuni  11300  reccn2ap  11320  isumz  11396  geoisum1c  11527  prod1dc  11593  efltim  11705  dvdsval2  11796  dvdscmulr  11826  dvdsmulcr  11827  modmulconst  11829  dvdsadd2b  11846  dvdsexp  11866  mulmoddvds  11868  divalglemeuneg  11927  zsupssdc  11954  gcdaddm  11984  dvdsgcdb  12013  mulgcd  12016  gcddiv  12019  uzwodc  12037  lcmdvdsb  12083  mulgcddvds  12093  qredeq  12095  divgcdcoprm0  12100  cncongr1  12102  euclemma  12145  rpexp  12152  rpexp12i  12154  fermltl  12233  prmdiv  12234  odzcllem  12241  odzdvds  12244  odzphi  12245  vfermltl  12250  coprimeprodsq  12256  pythagtriplem6  12269  pythagtriplem7  12270  pythagtriplem12  12274  pythagtriplem13  12275  pceu  12294  pcdvdsb  12318  pcgcd1  12326  dvdsprmpweq  12333  sumhashdc  12344  ctinf  12430  fvsetsid  12495  ressressg  12533  ressabsg  12534  rngplusgg  12594  imasaddvallemg  12735  qusaddvallemg  12751  plusfvalg  12781  mgmb1mgm1  12786  issubmnd  12842  ress0g  12843  grpasscan2  12933  grpidrcan  12934  grpidlcan  12935  grpinvadd  12947  grpsubeq0  12955  grppncan  12960  dfgrp3mlem  12967  dfgrp3me  12969  grpsubpropd2  12974  mhmmnd  12979  mulgnn0p1  12993  mulgnnsubcl  12994  mulgnn0subcl  12995  mulgsubcl  12996  mulgneg  13000  mulgaddcom  13005  mulginvcom  13006  subgcl  13042  subgsubcl  13043  subgsub  13044  subgmulg  13046  nsgconj  13064  nsgid  13073  ablinvadd  13111  ablsub4  13114  ablpncan2  13117  srgcl  13151  ringcl  13194  crngcom  13195  ringidss  13210  ringcom  13212  opprringbg  13248  unitmulcl  13280  unitmulclb  13281  dvrcl  13302  unitdvcl  13303  dvrcan1  13307  dvrcan3  13308  subrgmcl  13352  subrgdv  13357  islmod  13379  scafvalg  13395  2basgeng  13552  iuncld  13585  ntrss  13589  restco  13644  restabs  13645  cnprcl2k  13676  lmconst  13686  cnrest2  13706  cnmpt2t  13763  psmetsym  13799  psmetge0  13801  xmetge0  13835  xmetsym  13838  blvalps  13858  blval  13859  xblcntrps  13883  xblcntr  13884  xmssym  13939  blsscls2  13963  bdxmet  13971  txmetcnp  13988  dvfvalap  14120  dvid  14132  dvcnp2cntop  14133  rpcxpadd  14296  rpcxpsub  14299  rpmulcxp  14300  rpdivcxp  14302  cxpmul  14303  rpcxple2  14308  rpcxplt2  14309  rplogbval  14333  rplogbcl  14334  rplogbreexp  14341  relogbexpap  14346  logbleb  14349  logblt  14350  rplogbcxp  14351  rpcxplogb  14352  relogbcxpbap  14353  lgsneg1  14396  lgsmod  14397  lgsne0  14409  lgssq  14411  lgsdirnn0  14418  lgsdinn0  14419  findset  14667