Theorem simp2 1022

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

Syntax hints:   → wi 4   ∧ w3a 1002

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 1004

This theorem is referenced by:  simpl2  1025  simpr2  1028  simp2i  1031  simp2d  1034  simp12  1052  simp22  1055  simp32  1058  syld3an3  1316  3ianorr  1343  intn3an2d  1391  stoic4b  1475  nlim0  4489  tfisi  4683  sotri2  5132  sotri3  5133  feq123  5471  sefvex  5656  fvmptt  5734  fnfvima  5884  cocan1  5923  cocan2  5924  ovexg  6047  ovmpox  6145  ovmpoga  6146  fvmpopr2d  6153  caovimo  6211  tfr1onlembxssdm  6504  tfr1onlembfn  6505  tfrcllembxssdm  6517  tfrcllembfn  6518  freccllem  6563  frecfcllem  6565  frecsuclem  6567  frecrdg  6569  domssr  6946  mapxpen  7029  dif1en  7063  diffifi  7078  unsnfidcex  7107  unfidisj  7109  undifdc  7111  resfnfinfinss  7132  funrnfi  7135  sbthlemi9  7158  elfir  7166  difinfsn  7293  ctssdc  7306  djuassen  7425  xpdjuen  7426  mulcanenq  7598  ltanqg  7613  mulcanenq0ec  7658  addnnnq0  7662  distrprg  7801  aptipr  7854  addsrpr  7958  mulsrpr  7959  mulasssrg  7971  ltpsrprg  8016  axmulass  8086  axpre-ltadd  8099  subadd2  8376  nppcan  8394  nppcan3  8396  subsub2  8400  subsub4  8405  npncan3  8410  pnpcan  8411  pnncan  8413  subcan  8427  ltadd1  8602  leadd1  8603  leadd2  8604  ltsubadd  8605  ltsubadd2  8606  lesubadd  8607  lesubadd2  8608  ltaddsub  8609  leaddsub  8611  lesub1  8629  lesub2  8630  ltsub1  8631  ltsub2  8632  gt0add  8746  apreap  8760  lemul1  8766  reapmul1lem  8767  reapmul1  8768  reapadd1  8769  remulext1  8772  remulext2  8773  apadd2  8782  mulext2  8786  mulap0r  8788  leltap  8798  ltap  8806  apsub1  8815  recexaplem2  8825  mulcanap  8838  mulcanap2  8839  divvalap  8847  divmulap  8848  divcanap1  8854  diveqap0  8855  divap0b  8856  divrecap  8861  divassap  8863  div23ap  8864  divdirap  8870  divcanap3  8871  div11ap  8873  diveqap1  8878  divmuldivap  8885  divcanap5  8887  redivclap  8904  div2negap  8908  apmul1  8961  apmul2  8962  div2subap  9010  ltdiv1  9041  ledivmul  9050  lemuldiv  9054  lt2msq1  9058  ltdiv23  9065  squeeze0  9077  ofnegsub  9135  zaddcllemneg  9511  eluzsub  9779  nn01to3  9844  rpgecl  9910  addlelt  9996  xleadd1  10103  xltadd1  10104  lbioog  10141  ubioc1  10157  ubicc2  10213  icoshftf1o  10219  fzen  10271  nelfzo  10380  ubmelfzo  10438  ssfzo12  10462  ubmelm1fzo  10464  fzosplitprm1  10473  zsupssdc  10491  rebtwn2zlemshrink  10506  qbtwnre  10509  icogelb  10518  flqwordi  10541  flqword2  10542  flltdivnn0lt  10557  modqcl  10581  mulqmod0  10585  modqmulnn  10597  modqabs2  10613  modqmuladdnn0  10623  qnegmod  10624  addmodid  10627  modqm1p1mod0  10630  modifeq2int  10641  modqdi  10647  modqeqmodmin  10649  modfzo0difsn  10650  frec2uzf1od  10661  exp3val  10796  expnegap0  10802  expgt1  10832  exprecap  10835  expmulzap  10840  leexp2a  10847  expubnd  10851  mulbinom2  10911  bernneq2  10916  expnbnd  10918  fihashss  11073  fihashssdif  11075  fimaxq  11084  ccatval2  11168  ccatass  11178  ccatw2s1leng  11208  ccat2s1fvwd  11217  swrdval  11222  swrdnd  11233  pfxfv  11258  pfxpfx  11282  ccats1pfxeq  11288  ccats1pfxeqrex  11289  s3cl  11360  s3fv0g  11365  s3fv1g  11366  s3fv2g  11367  shftuz  11371  shftfibg  11374  cjdivap  11463  resqrtcl  11583  absdivap  11624  abssubne0  11645  maxleast  11767  lemininf  11788  ltmininf  11789  xrmaxltsup  11812  xrmaxaddlem  11814  xrmaxadd  11815  xrmineqinf  11823  xrltmininf  11824  xrminltinf  11826  xrminadd  11829  climuni  11847  reccn2ap  11867  isumz  11943  geoisum1c  12074  prod1dc  12140  efltim  12252  dvdsval2  12344  dvdscmulr  12374  dvdsmulcr  12375  modmulconst  12377  dvdsadd2b  12394  dvdsexp  12415  mulmoddvds  12417  divalglemeuneg  12477  gcdaddm  12548  dvdsgcdb  12577  mulgcd  12580  gcddiv  12583  uzwodc  12601  lcmdvdsb  12649  mulgcddvds  12659  qredeq  12661  divgcdcoprm0  12666  cncongr1  12668  euclemma  12711  rpexp  12718  rpexp12i  12720  fermltl  12799  prmdiv  12800  odzcllem  12808  odzdvds  12811  odzphi  12812  vfermltl  12817  coprimeprodsq  12823  pythagtriplem6  12836  pythagtriplem7  12837  pythagtriplem12  12841  pythagtriplem13  12842  pceu  12861  pcdvdsb  12886  pcgcd1  12894  dvdsprmpweq  12901  sumhashdc  12913  ctinf  13044  fvsetsid  13109  ressressg  13151  ressabsg  13152  rngplusgg  13213  imasaddvallemg  13391  qusaddvallemg  13409  plusfvalg  13439  mgmb1mgm1  13444  issubmnd  13518  ress0g  13519  imasmnd2  13528  imasmnd  13529  gsumfzz  13571  grpasscan2  13640  grpidrcan  13641  grpidlcan  13642  grpinvadd  13654  grpsubeq0  13662  grppncan  13667  dfgrp3mlem  13674  dfgrp3me  13676  grpsubpropd2  13681  pwsinvg  13688  imasgrp2  13690  imasgrp  13691  mhmmnd  13696  mulgnn0p1  13713  mulgnnsubcl  13714  mulgnn0subcl  13715  mulgsubcl  13716  mulgneg  13720  mulgaddcom  13726  mulginvcom  13727  submmulg  13746  subgcl  13764  subgsubcl  13765  subgsub  13766  subgmulg  13768  nsgconj  13786  nsgid  13795  quseccl0g  13811  ghmmulg  13836  ghmeqker  13851  f1ghm0to0  13852  kerf1ghm  13854  ablinvadd  13890  ablsub4  13893  ablpncan2  13896  subgabl  13912  gsumfzconst  13921  rngcl  13950  imasrng  13962  srgcl  13976  ringcl  14019  crngcom  14020  ringidss  14035  ringcom  14037  imasring  14070  opprringbg  14086  unitmulcl  14120  unitmulclb  14121  dvrcl  14142  unitdvcl  14143  dvrcan1  14147  dvrcan3  14148  rhmmul  14171  subrngrng  14209  subrngmcl  14216  subrgmcl  14240  subrgdv  14245  rrgeq0  14272  domneq0  14279  islmod  14298  scafvalg  14314  lmodcom  14340  rmodislmodlem  14357  rmodislmod  14358  lssclg  14371  lssvnegcl  14383  lssintclm  14391  lspss  14406  lspun  14409  lspsnvsi  14425  rspssp  14501  rnglidlmmgm  14503  rnglidlmsgrp  14504  rnglidlrng  14505  zndvds  14656  2basgeng  14799  iuncld  14832  ntrss  14836  restco  14891  restabs  14892  cnprcl2k  14923  lmconst  14933  cnrest2  14953  cnmpt2t  15010  psmetsym  15046  psmetge0  15048  xmetge0  15082  xmetsym  15085  blvalps  15105  blval  15106  xblcntrps  15130  xblcntr  15131  xmssym  15186  blsscls2  15210  bdxmet  15218  txmetcnp  15235  dvfvalap  15398  dvid  15412  dvidre  15414  dvcnp2cntop  15416  elplyr  15457  rpcxpadd  15622  rpcxpsub  15625  rpmulcxp  15626  rpdivcxp  15628  cxpmul  15629  rpcxple2  15635  rpcxplt2  15636  rplogbval  15662  rplogbcl  15663  rplogbreexp  15670  relogbexpap  15675  logbleb  15678  logblt  15679  rplogbcxp  15680  rpcxplogb  15681  relogbcxpbap  15682  sgmppw  15709  lgsneg1  15747  lgsmod  15748  lgsne0  15760  lgssq  15762  lgsdirnn0  15769  lgsdinn0  15770  lgsquad  15802  funvtxvalg  15880  funiedgvalg  15881  lpvtx  15923  ausgrumgrien  16014  ausgrusgrien  16015  wlkl1loop  16169  clwwlknonex2  16248  findset  16490