Theorem simp2 1025

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

Syntax hints:   → wi 4   ∧ w3a 1005

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 1007

This theorem is referenced by:  simpl2  1028  simpr2  1031  simp2i  1034  simp2d  1037  simp12  1055  simp22  1058  simp32  1061  syld3an3  1319  3ianorr  1346  intn3an2d  1394  stoic4b  1478  nlim0  4497  tfisi  4691  sotri2  5141  sotri3  5142  feq123  5481  sefvex  5669  fvmptt  5747  fnfvima  5899  cocan1  5938  cocan2  5939  ovexg  6062  ovmpox  6160  ovmpoga  6161  fvmpopr2d  6168  caovimo  6226  suppval1  6417  suppimacnvfn  6424  suppfnss  6435  tfr1onlembxssdm  6552  tfr1onlembfn  6553  tfrcllembxssdm  6565  tfrcllembfn  6566  freccllem  6611  frecfcllem  6613  frecsuclem  6615  frecrdg  6617  domssr  6994  mapxpen  7077  dif1en  7111  diffifi  7126  unsnfidcex  7155  unfidisj  7157  undifdc  7159  resfnfinfinss  7181  funrnfi  7184  sbthlemi9  7207  elfir  7215  difinfsn  7342  ctssdc  7355  djuassen  7475  xpdjuen  7476  mulcanenq  7648  ltanqg  7663  mulcanenq0ec  7708  addnnnq0  7712  distrprg  7851  aptipr  7904  addsrpr  8008  mulsrpr  8009  mulasssrg  8021  ltpsrprg  8066  axmulass  8136  axpre-ltadd  8149  subadd2  8426  nppcan  8444  nppcan3  8446  subsub2  8450  subsub4  8455  npncan3  8460  pnpcan  8461  pnncan  8463  subcan  8477  ltadd1  8652  leadd1  8653  leadd2  8654  ltsubadd  8655  ltsubadd2  8656  lesubadd  8657  lesubadd2  8658  ltaddsub  8659  leaddsub  8661  lesub1  8679  lesub2  8680  ltsub1  8681  ltsub2  8682  gt0add  8796  apreap  8810  lemul1  8816  reapmul1lem  8817  reapmul1  8818  reapadd1  8819  remulext1  8822  remulext2  8823  apadd2  8832  mulext2  8836  mulap0r  8838  leltap  8848  ltap  8856  apsub1  8865  recexaplem2  8875  mulcanap  8888  mulcanap2  8889  divvalap  8897  divmulap  8898  divcanap1  8904  diveqap0  8905  divap0b  8906  divrecap  8911  divassap  8913  div23ap  8914  divdirap  8920  divcanap3  8921  div11ap  8923  diveqap1  8928  divmuldivap  8935  divcanap5  8937  redivclap  8954  div2negap  8958  apmul1  9011  apmul2  9012  div2subap  9060  ltdiv1  9091  ledivmul  9100  lemuldiv  9104  lt2msq1  9108  ltdiv23  9115  squeeze0  9127  ofnegsub  9185  zaddcllemneg  9561  eluzsub  9829  nn01to3  9894  rpgecl  9960  addlelt  10046  xleadd1  10153  xltadd1  10154  lbioog  10191  ubioc1  10207  ubicc2  10263  icoshftf1o  10269  fzen  10321  nelfzo  10430  ubmelfzo  10489  ssfzo12  10513  ubmelm1fzo  10515  fzosplitprm1  10524  zsupssdc  10542  rebtwn2zlemshrink  10557  qbtwnre  10560  icogelb  10569  flqwordi  10592  flqword2  10593  flltdivnn0lt  10608  modqcl  10632  mulqmod0  10636  modqmulnn  10648  modqabs2  10664  modqmuladdnn0  10674  qnegmod  10675  addmodid  10678  modqm1p1mod0  10681  modifeq2int  10692  modqdi  10698  modqeqmodmin  10700  modfzo0difsn  10701  frec2uzf1od  10712  exp3val  10847  expnegap0  10853  expgt1  10883  exprecap  10886  expmulzap  10891  leexp2a  10898  expubnd  10902  mulbinom2  10962  bernneq2  10967  expnbnd  10969  fihashss  11124  fihashssdif  11126  fimaxq  11135  ccatval2  11222  ccatass  11232  ccatw2s1leng  11262  ccat2s1fvwd  11271  swrdval  11276  swrdnd  11287  pfxfv  11312  pfxpfx  11336  ccats1pfxeq  11342  ccats1pfxeqrex  11343  s3cl  11414  s3fv0g  11419  s3fv1g  11420  s3fv2g  11421  shftuz  11438  shftfibg  11441  cjdivap  11530  resqrtcl  11650  absdivap  11691  abssubne0  11712  maxleast  11834  lemininf  11855  ltmininf  11856  xrmaxltsup  11879  xrmaxaddlem  11881  xrmaxadd  11882  xrmineqinf  11890  xrltmininf  11891  xrminltinf  11893  xrminadd  11896  climuni  11914  reccn2ap  11934  isumz  12011  geoisum1c  12142  prod1dc  12208  efltim  12320  dvdsval2  12412  dvdscmulr  12442  dvdsmulcr  12443  modmulconst  12445  dvdsadd2b  12462  dvdsexp  12483  mulmoddvds  12485  divalglemeuneg  12545  gcdaddm  12616  dvdsgcdb  12645  mulgcd  12648  gcddiv  12651  uzwodc  12669  lcmdvdsb  12717  mulgcddvds  12727  qredeq  12729  divgcdcoprm0  12734  cncongr1  12736  euclemma  12779  rpexp  12786  rpexp12i  12788  fermltl  12867  prmdiv  12868  odzcllem  12876  odzdvds  12879  odzphi  12880  vfermltl  12885  coprimeprodsq  12891  pythagtriplem6  12904  pythagtriplem7  12905  pythagtriplem12  12909  pythagtriplem13  12910  pceu  12929  pcdvdsb  12954  pcgcd1  12962  dvdsprmpweq  12969  sumhashdc  12981  ctinf  13112  fvsetsid  13177  ressressg  13219  ressabsg  13220  rngplusgg  13281  imasaddvallemg  13459  qusaddvallemg  13477  plusfvalg  13507  mgmb1mgm1  13512  issubmnd  13586  ress0g  13587  imasmnd2  13596  imasmnd  13597  gsumfzz  13639  grpasscan2  13708  grpidrcan  13709  grpidlcan  13710  grpinvadd  13722  grpsubeq0  13730  grppncan  13735  dfgrp3mlem  13742  dfgrp3me  13744  grpsubpropd2  13749  pwsinvg  13756  imasgrp2  13758  imasgrp  13759  mhmmnd  13764  mulgnn0p1  13781  mulgnnsubcl  13782  mulgnn0subcl  13783  mulgsubcl  13784  mulgneg  13788  mulgaddcom  13794  mulginvcom  13795  submmulg  13814  subgcl  13832  subgsubcl  13833  subgsub  13834  subgmulg  13836  nsgconj  13854  nsgid  13863  quseccl0g  13879  ghmmulg  13904  ghmeqker  13919  f1ghm0to0  13920  kerf1ghm  13922  ablinvadd  13958  ablsub4  13961  ablpncan2  13964  subgabl  13980  gsumfzconst  13989  rngcl  14019  imasrng  14031  srgcl  14045  ringcl  14088  crngcom  14089  ringidss  14104  ringcom  14106  imasring  14139  opprringbg  14155  unitmulcl  14189  unitmulclb  14190  dvrcl  14211  unitdvcl  14212  dvrcan1  14216  dvrcan3  14217  rhmmul  14240  subrngrng  14278  subrngmcl  14285  subrgmcl  14309  subrgdv  14314  rrgeq0  14341  domneq0  14348  islmod  14367  scafvalg  14383  lmodcom  14409  rmodislmodlem  14426  rmodislmod  14427  lssclg  14440  lssvnegcl  14452  lssintclm  14460  lspss  14475  lspun  14478  lspsnvsi  14494  rspssp  14570  rnglidlmmgm  14572  rnglidlmsgrp  14573  rnglidlrng  14574  zndvds  14725  psrbaglecl  14751  psrbagcon  14752  2basgeng  14873  iuncld  14906  ntrss  14910  restco  14965  restabs  14966  cnprcl2k  14997  lmconst  15007  cnrest2  15027  cnmpt2t  15084  psmetsym  15120  psmetge0  15122  xmetge0  15156  xmetsym  15159  blvalps  15179  blval  15180  xblcntrps  15204  xblcntr  15205  xmssym  15260  blsscls2  15284  bdxmet  15292  txmetcnp  15309  dvfvalap  15472  dvid  15486  dvidre  15488  dvcnp2cntop  15490  elplyr  15531  rpcxpadd  15696  rpcxpsub  15699  rpmulcxp  15700  rpdivcxp  15702  cxpmul  15703  rpcxple2  15709  rpcxplt2  15710  rplogbval  15736  rplogbcl  15737  rplogbreexp  15744  relogbexpap  15749  logbleb  15752  logblt  15753  rplogbcxp  15754  rpcxplogb  15755  relogbcxpbap  15756  sgmppw  15783  lgsneg1  15821  lgsmod  15822  lgsne0  15834  lgssq  15836  lgsdirnn0  15843  lgsdinn0  15844  lgsquad  15876  funvtxvalg  15954  funiedgvalg  15955  lpvtx  15997  ausgrumgrien  16088  ausgrusgrien  16089  uhgrissubgr  16179  egrsubgr  16181  subumgredg2en  16189  subusgr  16193  wlkl1loop  16276  clwwlknonex2  16357  eulerpathprum  16398  eulerpathum  16399  findset  16638  repiecele0  16735  repiecege0  16736  gfsumsn  16791