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  4412  tfisi  4604  sotri2  5044  sotri3  5045  feq123  5376  sefvex  5555  fvmptt  5627  fnfvima  5771  cocan1  5808  cocan2  5809  ovexg  5929  ovmpox  6024  ovmpoga  6025  caovimo  6089  tfr1onlembxssdm  6367  tfr1onlembfn  6368  tfrcllembxssdm  6380  tfrcllembfn  6381  freccllem  6426  frecfcllem  6428  frecsuclem  6430  frecrdg  6432  mapxpen  6875  dif1en  6906  diffifi  6921  unsnfidcex  6947  unfidisj  6949  undifdc  6951  resfnfinfinss  6968  funrnfi  6970  sbthlemi9  6993  elfir  7001  difinfsn  7128  ctssdc  7141  djuassen  7245  xpdjuen  7246  mulcanenq  7413  ltanqg  7428  mulcanenq0ec  7473  addnnnq0  7477  distrprg  7616  aptipr  7669  addsrpr  7773  mulsrpr  7774  mulasssrg  7786  ltpsrprg  7831  axmulass  7901  axpre-ltadd  7914  subadd2  8190  nppcan  8208  nppcan3  8210  subsub2  8214  subsub4  8219  npncan3  8224  pnpcan  8225  pnncan  8227  subcan  8241  ltadd1  8415  leadd1  8416  leadd2  8417  ltsubadd  8418  ltsubadd2  8419  lesubadd  8420  lesubadd2  8421  ltaddsub  8422  leaddsub  8424  lesub1  8442  lesub2  8443  ltsub1  8444  ltsub2  8445  gt0add  8559  apreap  8573  lemul1  8579  reapmul1lem  8580  reapmul1  8581  reapadd1  8582  remulext1  8585  remulext2  8586  apadd2  8595  mulext2  8599  mulap0r  8601  leltap  8611  ltap  8619  apsub1  8628  recexaplem2  8638  mulcanap  8651  mulcanap2  8652  divvalap  8660  divmulap  8661  divcanap1  8667  diveqap0  8668  divap0b  8669  divrecap  8674  divassap  8676  div23ap  8677  divdirap  8683  divcanap3  8684  div11ap  8686  diveqap1  8691  divmuldivap  8698  divcanap5  8700  redivclap  8717  div2negap  8721  apmul1  8774  apmul2  8775  div2subap  8823  ltdiv1  8854  ledivmul  8863  lemuldiv  8867  lt2msq1  8871  ltdiv23  8878  squeeze0  8890  zaddcllemneg  9321  eluzsub  9586  nn01to3  9646  rpgecl  9711  addlelt  9797  xleadd1  9904  xltadd1  9905  lbioog  9942  ubioc1  9958  ubicc2  10014  icoshftf1o  10020  fzen  10072  ubmelfzo  10229  ssfzo12  10253  ubmelm1fzo  10255  fzosplitprm1  10263  rebtwn2zlemshrink  10283  qbtwnre  10286  icogelb  10295  flqwordi  10318  flqword2  10319  flltdivnn0lt  10334  modqcl  10356  mulqmod0  10360  modqmulnn  10372  modqabs2  10388  modqmuladdnn0  10398  qnegmod  10399  addmodid  10402  modqm1p1mod0  10405  modifeq2int  10416  modqdi  10422  modqeqmodmin  10424  modfzo0difsn  10425  frec2uzf1od  10436  exp3val  10552  expnegap0  10558  expgt1  10588  exprecap  10591  expmulzap  10596  leexp2a  10603  expubnd  10607  mulbinom2  10667  bernneq2  10672  expnbnd  10674  fihashss  10827  fihashssdif  10829  fimaxq  10838  shftuz  10857  shftfibg  10860  cjdivap  10949  resqrtcl  11069  absdivap  11110  abssubne0  11131  maxleast  11253  lemininf  11273  ltmininf  11274  xrmaxltsup  11297  xrmaxaddlem  11299  xrmaxadd  11300  xrmineqinf  11308  xrltmininf  11309  xrminltinf  11311  xrminadd  11314  climuni  11332  reccn2ap  11352  isumz  11428  geoisum1c  11559  prod1dc  11625  efltim  11737  dvdsval2  11828  dvdscmulr  11858  dvdsmulcr  11859  modmulconst  11861  dvdsadd2b  11878  dvdsexp  11898  mulmoddvds  11900  divalglemeuneg  11959  zsupssdc  11986  gcdaddm  12016  dvdsgcdb  12045  mulgcd  12048  gcddiv  12051  uzwodc  12069  lcmdvdsb  12115  mulgcddvds  12125  qredeq  12127  divgcdcoprm0  12132  cncongr1  12134  euclemma  12177  rpexp  12184  rpexp12i  12186  fermltl  12265  prmdiv  12266  odzcllem  12273  odzdvds  12276  odzphi  12277  vfermltl  12282  coprimeprodsq  12288  pythagtriplem6  12301  pythagtriplem7  12302  pythagtriplem12  12306  pythagtriplem13  12307  pceu  12326  pcdvdsb  12351  pcgcd1  12359  dvdsprmpweq  12366  sumhashdc  12378  ctinf  12480  fvsetsid  12545  ressressg  12584  ressabsg  12585  rngplusgg  12645  imasaddvallemg  12789  qusaddvallemg  12806  plusfvalg  12836  mgmb1mgm1  12841  issubmnd  12900  ress0g  12901  grpasscan2  13005  grpidrcan  13006  grpidlcan  13007  grpinvadd  13019  grpsubeq0  13027  grppncan  13032  dfgrp3mlem  13039  dfgrp3me  13041  grpsubpropd2  13046  imasgrp2  13049  imasgrp  13050  mhmmnd  13055  mulgnn0p1  13070  mulgnnsubcl  13071  mulgnn0subcl  13072  mulgsubcl  13073  mulgneg  13077  mulgaddcom  13083  mulginvcom  13084  subgcl  13120  subgsubcl  13121  subgsub  13122  subgmulg  13124  nsgconj  13142  nsgid  13151  quseccl0g  13167  ghmmulg  13192  ghmeqker  13207  f1ghm0to0  13208  kerf1ghm  13210  ablinvadd  13246  ablsub4  13249  ablpncan2  13252  subgabl  13266  rngcl  13295  imasrng  13307  srgcl  13321  ringcl  13364  crngcom  13365  ringidss  13380  ringcom  13382  imasring  13411  opprringbg  13427  unitmulcl  13460  unitmulclb  13461  dvrcl  13482  unitdvcl  13483  dvrcan1  13487  dvrcan3  13488  rhmmul  13511  subrngrng  13546  subrngmcl  13553  subrgmcl  13577  subrgdv  13582  islmod  13604  scafvalg  13620  lmodcom  13646  rmodislmodlem  13663  rmodislmod  13664  lssclg  13677  lssvnegcl  13689  lssintclm  13697  lspss  13712  lspun  13715  lspsnvsi  13731  rspssp  13807  rnglidlmmgm  13809  rnglidlmsgrp  13810  rnglidlrng  13811  2basgeng  14034  iuncld  14067  ntrss  14071  restco  14126  restabs  14127  cnprcl2k  14158  lmconst  14168  cnrest2  14188  cnmpt2t  14245  psmetsym  14281  psmetge0  14283  xmetge0  14317  xmetsym  14320  blvalps  14340  blval  14341  xblcntrps  14365  xblcntr  14366  xmssym  14421  blsscls2  14445  bdxmet  14453  txmetcnp  14470  dvfvalap  14602  dvid  14614  dvcnp2cntop  14615  rpcxpadd  14778  rpcxpsub  14781  rpmulcxp  14782  rpdivcxp  14784  cxpmul  14785  rpcxple2  14790  rpcxplt2  14791  rplogbval  14815  rplogbcl  14816  rplogbreexp  14823  relogbexpap  14828  logbleb  14831  logblt  14832  rplogbcxp  14833  rpcxplogb  14834  relogbcxpbap  14835  lgsneg1  14879  lgsmod  14880  lgsne0  14892  lgssq  14894  lgsdirnn0  14901  lgsdinn0  14902  findset  15150