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  4517  tfisi  4711  sotri2  5162  sotri3  5163  feq123  5502  sefvex  5693  fvmptt  5771  fnfvima  5923  cocan1  5962  cocan2  5963  ovexg  6086  ovmpox  6184  ovmpoga  6185  fvmpopr2d  6192  caovimo  6250  suppval1  6441  suppimacnvfn  6448  suppfnss  6459  tfr1onlembxssdm  6576  tfr1onlembfn  6577  tfrcllembxssdm  6589  tfrcllembfn  6590  freccllem  6635  frecfcllem  6637  frecsuclem  6639  frecrdg  6641  domssr  7019  mapxpen  7103  dif1en  7138  diffifi  7153  unsnfidcex  7182  unfidisj  7184  undifdc  7186  resfnfinfinss  7208  funrnfi  7211  fissfi  7218  sbthlemi9  7237  elfir  7262  difinfsn  7393  ctssdc  7406  djuassen  7526  xpdjuen  7527  mulcanenq  7705  ltanqg  7720  mulcanenq0ec  7765  addnnnq0  7769  distrprg  7908  aptipr  7961  addsrpr  8065  mulsrpr  8066  mulasssrg  8078  ltpsrprg  8123  axmulass  8193  axpre-ltadd  8206  subadd2  8482  nppcan  8500  nppcan3  8502  subsub2  8506  subsub4  8511  npncan3  8516  pnpcan  8517  pnncan  8519  subcan  8533  ltadd1  8708  leadd1  8709  leadd2  8710  ltsubadd  8711  ltsubadd2  8712  lesubadd  8713  lesubadd2  8714  ltaddsub  8715  leaddsub  8717  lesub1  8735  lesub2  8736  ltsub1  8737  ltsub2  8738  gt0add  8852  apreap  8866  lemul1  8872  reapmul1lem  8873  reapmul1  8874  reapadd1  8875  remulext1  8878  remulext2  8879  apadd2  8888  mulext2  8892  mulap0r  8894  leltap  8904  ltap  8912  apsub1  8921  recexaplem2  8931  mulcanap  8944  mulcanap2  8945  divvalap  8953  divmulap  8954  divcanap1  8960  diveqap0  8961  divap0b  8962  divrecap  8967  divassap  8969  div23ap  8970  divdirap  8976  divcanap3  8977  div11ap  8979  diveqap1  8984  divmuldivap  8991  divcanap5  8993  redivclap  9010  div2negap  9014  apmul1  9067  apmul2  9068  div2subap  9116  ltdiv1  9147  ledivmul  9156  lemuldiv  9160  lt2msq1  9164  ltdiv23  9171  squeeze0  9183  ofnegsub  9241  zaddcllemneg  9621  zfidc  9661  eluzsub  9890  nn01to3  9955  rpgecl  10021  addlelt  10107  xleadd1  10214  xltadd1  10215  lbioog  10252  ubioc1  10268  ubicc2  10324  icoshftf1o  10330  fzen  10383  nelfzo  10493  ubmelfzo  10552  ssfzo12  10576  ubmelm1fzo  10578  fzosplitprm1  10587  zsupssdc  10605  rebtwn2zlemshrink  10620  qbtwnre  10623  icogelb  10632  flqwordi  10655  flqword2  10656  flltdivnn0lt  10671  modqcl  10695  mulqmod0  10699  modqmulnn  10711  modqabs2  10727  modqmuladdnn0  10737  qnegmod  10738  addmodid  10741  modqm1p1mod0  10744  modifeq2int  10755  modqdi  10761  modqeqmodmin  10763  modfzo0difsn  10764  frec2uzf1od  10775  exp3val  10910  expnegap0  10916  expgt1  10946  exprecap  10949  expmulzap  10954  leexp2a  10961  expubnd  10965  mulbinom2  11025  bernneq2  11031  expnbnd  11033  fihashss  11189  fihashssdif  11191  fimaxq  11202  ccatval2  11294  ccatass  11304  ccatw2s1leng  11334  ccat2s1fvwd  11343  swrdval  11348  swrdnd  11359  pfxfv  11384  pfxpfx  11408  ccats1pfxeq  11414  ccats1pfxeqrex  11415  s3cl  11486  s3fv0g  11491  s3fv1g  11492  s3fv2g  11493  shftuz  11510  shftfibg  11513  cjdivap  11602  resqrtcl  11722  absdivap  11763  abssubne0  11784  maxleast  11906  lemininf  11927  ltmininf  11928  xrmaxltsup  11951  xrmaxaddlem  11953  xrmaxadd  11954  xrmineqinf  11962  xrltmininf  11963  xrminltinf  11965  xrminadd  11968  climuni  11986  reccn2ap  12006  isumz  12083  geoisum1c  12214  prod1dc  12280  efltim  12392  dvdsval2  12484  dvdscmulr  12514  dvdsmulcr  12515  modmulconst  12517  dvdsadd2b  12534  dvdsexp  12555  mulmoddvds  12557  divalglemeuneg  12617  gcdaddm  12688  dvdsgcdb  12717  mulgcd  12720  gcddiv  12723  uzwodc  12741  lcmdvdsb  12789  mulgcddvds  12799  qredeq  12801  divgcdcoprm0  12806  cncongr1  12808  euclemma  12851  rpexp  12858  rpexp12i  12860  fermltl  12939  prmdiv  12940  odzcllem  12948  odzdvds  12951  odzphi  12952  vfermltl  12957  coprimeprodsq  12963  pythagtriplem6  12976  pythagtriplem7  12977  pythagtriplem12  12981  pythagtriplem13  12982  pceu  13001  pcdvdsb  13026  pcgcd1  13034  dvdsprmpweq  13041  sumhashdc  13053  ctinf  13202  fvsetsid  13267  ressressg  13309  ressabsg  13310  rngplusgg  13371  imasaddvallemg  13549  qusaddvallemg  13567  plusfvalg  13597  mgmb1mgm1  13602  issubmnd  13676  ress0g  13677  imasmnd2  13686  imasmnd  13687  gsumfzz  13729  grpasscan2  13798  grpidrcan  13799  grpidlcan  13800  grpinvadd  13812  grpsubeq0  13820  grppncan  13825  dfgrp3mlem  13832  dfgrp3me  13834  grpsubpropd2  13839  pwsinvg  13846  imasgrp2  13848  imasgrp  13849  mhmmnd  13854  mulgnn0p1  13871  mulgnnsubcl  13872  mulgnn0subcl  13873  mulgsubcl  13874  mulgneg  13878  mulgaddcom  13884  mulginvcom  13885  submmulg  13904  subgcl  13922  subgsubcl  13923  subgsub  13924  subgmulg  13926  nsgconj  13944  nsgid  13953  quseccl0g  13969  ghmmulg  13994  ghmeqker  14009  f1ghm0to0  14010  kerf1ghm  14012  ablinvadd  14048  ablsub4  14051  ablpncan2  14054  subgabl  14070  gsumfzconst  14079  rngcl  14109  imasrng  14121  srgcl  14135  ringcl  14178  crngcom  14179  ringidss  14194  ringcom  14196  imasring  14229  opprringbg  14245  unitmulcl  14280  unitmulclb  14281  dvrcl  14302  unitdvcl  14303  dvrcan1  14307  dvrcan3  14308  rhmmul  14331  subrngrng  14370  subrngmcl  14377  subrgmcl  14401  subrgdv  14406  rrgeq0  14433  domneq0  14441  islmod  14488  scafvalg  14504  lmodcom  14530  rmodislmodlem  14547  rmodislmod  14548  lssclg  14561  lssvnegcl  14573  lssintclm  14581  lspss  14596  lspun  14599  lspsnvsi  14615  rspssp  14691  rnglidlmmgm  14693  rnglidlmsgrp  14694  rnglidlrng  14695  zndvds  14846  psrbaglecl  14873  psrbagcon  14875  2basgeng  14996  iuncld  15029  ntrss  15033  restco  15088  restabs  15089  cnprcl2k  15120  lmconst  15130  cnrest2  15150  cnmpt2t  15207  psmetsym  15243  psmetge0  15245  xmetge0  15279  xmetsym  15282  blvalps  15302  blval  15303  xblcntrps  15327  xblcntr  15328  xmssym  15383  blsscls2  15407  bdxmet  15415  txmetcnp  15432  dvfvalap  15595  dvid  15609  dvidre  15611  dvcnp2cntop  15613  elplyr  15654  rpcxpadd  15819  rpcxpsub  15822  rpmulcxp  15823  rpdivcxp  15825  cxpmul  15826  rpcxple2  15832  rpcxplt2  15833  rplogbval  15859  rplogbcl  15860  rplogbreexp  15867  relogbexpap  15872  logbleb  15875  logblt  15876  rplogbcxp  15877  rpcxplogb  15878  relogbcxpbap  15879  sgmppw  15909  lgsneg1  15947  lgsmod  15948  lgsne0  15960  lgssq  15962  lgsdirnn0  15969  lgsdinn0  15970  lgsquad  16002  funvtxvalg  16080  funiedgvalg  16081  lpvtx  16123  ausgrumgrien  16214  ausgrusgrien  16215  uhgrissubgr  16305  egrsubgr  16307  subumgredg2en  16315  subusgr  16319  wlkl1loop  16402  clwwlknonex2  16483  eulerpathprum  16524  eulerpathum  16525  findset  16764  repiecele0  16859  repiecege0  16860  gfsumsn  16916