Theorem simp2 1001

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

Syntax hints:   → wi 4   ∧ w3a 981

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 983

This theorem is referenced by:  simpl2  1004  simpr2  1007  simp2i  1010  simp2d  1013  simp12  1031  simp22  1034  simp32  1037  syld3an3  1295  3ianorr  1322  intn3an2d  1369  stoic4b  1453  nlim0  4445  tfisi  4639  sotri2  5085  sotri3  5086  feq123  5423  sefvex  5604  fvmptt  5678  fnfvima  5826  cocan1  5863  cocan2  5864  ovexg  5985  ovmpox  6081  ovmpoga  6082  fvmpopr2d  6089  caovimo  6147  tfr1onlembxssdm  6436  tfr1onlembfn  6437  tfrcllembxssdm  6449  tfrcllembfn  6450  freccllem  6495  frecfcllem  6497  frecsuclem  6499  frecrdg  6501  domssr  6876  mapxpen  6952  dif1en  6983  diffifi  6998  unsnfidcex  7024  unfidisj  7026  undifdc  7028  resfnfinfinss  7048  funrnfi  7051  sbthlemi9  7074  elfir  7082  difinfsn  7209  ctssdc  7222  djuassen  7336  xpdjuen  7337  mulcanenq  7505  ltanqg  7520  mulcanenq0ec  7565  addnnnq0  7569  distrprg  7708  aptipr  7761  addsrpr  7865  mulsrpr  7866  mulasssrg  7878  ltpsrprg  7923  axmulass  7993  axpre-ltadd  8006  subadd2  8283  nppcan  8301  nppcan3  8303  subsub2  8307  subsub4  8312  npncan3  8317  pnpcan  8318  pnncan  8320  subcan  8334  ltadd1  8509  leadd1  8510  leadd2  8511  ltsubadd  8512  ltsubadd2  8513  lesubadd  8514  lesubadd2  8515  ltaddsub  8516  leaddsub  8518  lesub1  8536  lesub2  8537  ltsub1  8538  ltsub2  8539  gt0add  8653  apreap  8667  lemul1  8673  reapmul1lem  8674  reapmul1  8675  reapadd1  8676  remulext1  8679  remulext2  8680  apadd2  8689  mulext2  8693  mulap0r  8695  leltap  8705  ltap  8713  apsub1  8722  recexaplem2  8732  mulcanap  8745  mulcanap2  8746  divvalap  8754  divmulap  8755  divcanap1  8761  diveqap0  8762  divap0b  8763  divrecap  8768  divassap  8770  div23ap  8771  divdirap  8777  divcanap3  8778  div11ap  8780  diveqap1  8785  divmuldivap  8792  divcanap5  8794  redivclap  8811  div2negap  8815  apmul1  8868  apmul2  8869  div2subap  8917  ltdiv1  8948  ledivmul  8957  lemuldiv  8961  lt2msq1  8965  ltdiv23  8972  squeeze0  8984  ofnegsub  9042  zaddcllemneg  9418  eluzsub  9685  nn01to3  9745  rpgecl  9811  addlelt  9897  xleadd1  10004  xltadd1  10005  lbioog  10042  ubioc1  10058  ubicc2  10114  icoshftf1o  10120  fzen  10172  nelfzo  10281  ubmelfzo  10336  ssfzo12  10360  ubmelm1fzo  10362  fzosplitprm1  10370  zsupssdc  10388  rebtwn2zlemshrink  10403  qbtwnre  10406  icogelb  10415  flqwordi  10438  flqword2  10439  flltdivnn0lt  10454  modqcl  10478  mulqmod0  10482  modqmulnn  10494  modqabs2  10510  modqmuladdnn0  10520  qnegmod  10521  addmodid  10524  modqm1p1mod0  10527  modifeq2int  10538  modqdi  10544  modqeqmodmin  10546  modfzo0difsn  10547  frec2uzf1od  10558  exp3val  10693  expnegap0  10699  expgt1  10729  exprecap  10732  expmulzap  10737  leexp2a  10744  expubnd  10748  mulbinom2  10808  bernneq2  10813  expnbnd  10815  fihashss  10968  fihashssdif  10970  fimaxq  10979  ccatval2  11062  ccatass  11072  swrdval  11109  swrdnd  11120  pfxfv  11143  pfxpfx  11167  shftuz  11172  shftfibg  11175  cjdivap  11264  resqrtcl  11384  absdivap  11425  abssubne0  11446  maxleast  11568  lemininf  11589  ltmininf  11590  xrmaxltsup  11613  xrmaxaddlem  11615  xrmaxadd  11616  xrmineqinf  11624  xrltmininf  11625  xrminltinf  11627  xrminadd  11630  climuni  11648  reccn2ap  11668  isumz  11744  geoisum1c  11875  prod1dc  11941  efltim  12053  dvdsval2  12145  dvdscmulr  12175  dvdsmulcr  12176  modmulconst  12178  dvdsadd2b  12195  dvdsexp  12216  mulmoddvds  12218  divalglemeuneg  12278  gcdaddm  12349  dvdsgcdb  12378  mulgcd  12381  gcddiv  12384  uzwodc  12402  lcmdvdsb  12450  mulgcddvds  12460  qredeq  12462  divgcdcoprm0  12467  cncongr1  12469  euclemma  12512  rpexp  12519  rpexp12i  12521  fermltl  12600  prmdiv  12601  odzcllem  12609  odzdvds  12612  odzphi  12613  vfermltl  12618  coprimeprodsq  12624  pythagtriplem6  12637  pythagtriplem7  12638  pythagtriplem12  12642  pythagtriplem13  12643  pceu  12662  pcdvdsb  12687  pcgcd1  12695  dvdsprmpweq  12702  sumhashdc  12714  ctinf  12845  fvsetsid  12910  ressressg  12951  ressabsg  12952  rngplusgg  13013  imasaddvallemg  13191  qusaddvallemg  13209  plusfvalg  13239  mgmb1mgm1  13244  issubmnd  13318  ress0g  13319  imasmnd2  13328  imasmnd  13329  gsumfzz  13371  grpasscan2  13440  grpidrcan  13441  grpidlcan  13442  grpinvadd  13454  grpsubeq0  13462  grppncan  13467  dfgrp3mlem  13474  dfgrp3me  13476  grpsubpropd2  13481  pwsinvg  13488  imasgrp2  13490  imasgrp  13491  mhmmnd  13496  mulgnn0p1  13513  mulgnnsubcl  13514  mulgnn0subcl  13515  mulgsubcl  13516  mulgneg  13520  mulgaddcom  13526  mulginvcom  13527  submmulg  13546  subgcl  13564  subgsubcl  13565  subgsub  13566  subgmulg  13568  nsgconj  13586  nsgid  13595  quseccl0g  13611  ghmmulg  13636  ghmeqker  13651  f1ghm0to0  13652  kerf1ghm  13654  ablinvadd  13690  ablsub4  13693  ablpncan2  13696  subgabl  13712  gsumfzconst  13721  rngcl  13750  imasrng  13762  srgcl  13776  ringcl  13819  crngcom  13820  ringidss  13835  ringcom  13837  imasring  13870  opprringbg  13886  unitmulcl  13919  unitmulclb  13920  dvrcl  13941  unitdvcl  13942  dvrcan1  13946  dvrcan3  13947  rhmmul  13970  subrngrng  14008  subrngmcl  14015  subrgmcl  14039  subrgdv  14044  rrgeq0  14071  domneq0  14078  islmod  14097  scafvalg  14113  lmodcom  14139  rmodislmodlem  14156  rmodislmod  14157  lssclg  14170  lssvnegcl  14182  lssintclm  14190  lspss  14205  lspun  14208  lspsnvsi  14224  rspssp  14300  rnglidlmmgm  14302  rnglidlmsgrp  14303  rnglidlrng  14304  zndvds  14455  2basgeng  14598  iuncld  14631  ntrss  14635  restco  14690  restabs  14691  cnprcl2k  14722  lmconst  14732  cnrest2  14752  cnmpt2t  14809  psmetsym  14845  psmetge0  14847  xmetge0  14881  xmetsym  14884  blvalps  14904  blval  14905  xblcntrps  14929  xblcntr  14930  xmssym  14985  blsscls2  15009  bdxmet  15017  txmetcnp  15034  dvfvalap  15197  dvid  15211  dvidre  15213  dvcnp2cntop  15215  elplyr  15256  rpcxpadd  15421  rpcxpsub  15424  rpmulcxp  15425  rpdivcxp  15427  cxpmul  15428  rpcxple2  15434  rpcxplt2  15435  rplogbval  15461  rplogbcl  15462  rplogbreexp  15469  relogbexpap  15474  logbleb  15477  logblt  15478  rplogbcxp  15479  rpcxplogb  15480  relogbcxpbap  15481  sgmppw  15508  lgsneg1  15546  lgsmod  15547  lgsne0  15559  lgssq  15561  lgsdirnn0  15568  lgsdinn0  15569  lgsquad  15601  funvtxvalg  15679  funiedgvalg  15680  lpvtx  15719  findset  15955