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  4514  tfisi  4708  sotri2  5159  sotri3  5160  feq123  5499  sefvex  5690  fvmptt  5768  fnfvima  5920  cocan1  5959  cocan2  5960  ovexg  6083  ovmpox  6181  ovmpoga  6182  fvmpopr2d  6189  caovimo  6247  suppval1  6438  suppimacnvfn  6445  suppfnss  6456  tfr1onlembxssdm  6573  tfr1onlembfn  6574  tfrcllembxssdm  6586  tfrcllembfn  6587  freccllem  6632  frecfcllem  6634  frecsuclem  6636  frecrdg  6638  domssr  7016  mapxpen  7100  dif1en  7135  diffifi  7150  unsnfidcex  7179  unfidisj  7181  undifdc  7183  resfnfinfinss  7205  funrnfi  7208  fissfi  7215  sbthlemi9  7234  elfir  7259  difinfsn  7390  ctssdc  7403  djuassen  7523  xpdjuen  7524  mulcanenq  7696  ltanqg  7711  mulcanenq0ec  7756  addnnnq0  7760  distrprg  7899  aptipr  7952  addsrpr  8056  mulsrpr  8057  mulasssrg  8069  ltpsrprg  8114  axmulass  8184  axpre-ltadd  8197  subadd2  8473  nppcan  8491  nppcan3  8493  subsub2  8497  subsub4  8502  npncan3  8507  pnpcan  8508  pnncan  8510  subcan  8524  ltadd1  8699  leadd1  8700  leadd2  8701  ltsubadd  8702  ltsubadd2  8703  lesubadd  8704  lesubadd2  8705  ltaddsub  8706  leaddsub  8708  lesub1  8726  lesub2  8727  ltsub1  8728  ltsub2  8729  gt0add  8843  apreap  8857  lemul1  8863  reapmul1lem  8864  reapmul1  8865  reapadd1  8866  remulext1  8869  remulext2  8870  apadd2  8879  mulext2  8883  mulap0r  8885  leltap  8895  ltap  8903  apsub1  8912  recexaplem2  8922  mulcanap  8935  mulcanap2  8936  divvalap  8944  divmulap  8945  divcanap1  8951  diveqap0  8952  divap0b  8953  divrecap  8958  divassap  8960  div23ap  8961  divdirap  8967  divcanap3  8968  div11ap  8970  diveqap1  8975  divmuldivap  8982  divcanap5  8984  redivclap  9001  div2negap  9005  apmul1  9058  apmul2  9059  div2subap  9107  ltdiv1  9138  ledivmul  9147  lemuldiv  9151  lt2msq1  9155  ltdiv23  9162  squeeze0  9174  ofnegsub  9232  zaddcllemneg  9612  eluzsub  9880  nn01to3  9945  rpgecl  10011  addlelt  10097  xleadd1  10204  xltadd1  10205  lbioog  10242  ubioc1  10258  ubicc2  10314  icoshftf1o  10320  fzen  10373  nelfzo  10482  ubmelfzo  10541  ssfzo12  10565  ubmelm1fzo  10567  fzosplitprm1  10576  zsupssdc  10594  rebtwn2zlemshrink  10609  qbtwnre  10612  icogelb  10621  flqwordi  10644  flqword2  10645  flltdivnn0lt  10660  modqcl  10684  mulqmod0  10688  modqmulnn  10700  modqabs2  10716  modqmuladdnn0  10726  qnegmod  10727  addmodid  10730  modqm1p1mod0  10733  modifeq2int  10744  modqdi  10750  modqeqmodmin  10752  modfzo0difsn  10753  frec2uzf1od  10764  exp3val  10899  expnegap0  10905  expgt1  10935  exprecap  10938  expmulzap  10943  leexp2a  10950  expubnd  10954  mulbinom2  11014  bernneq2  11019  expnbnd  11021  fihashss  11176  fihashssdif  11178  fimaxq  11187  ccatval2  11279  ccatass  11289  ccatw2s1leng  11319  ccat2s1fvwd  11328  swrdval  11333  swrdnd  11344  pfxfv  11369  pfxpfx  11393  ccats1pfxeq  11399  ccats1pfxeqrex  11400  s3cl  11471  s3fv0g  11476  s3fv1g  11477  s3fv2g  11478  shftuz  11495  shftfibg  11498  cjdivap  11587  resqrtcl  11707  absdivap  11748  abssubne0  11769  maxleast  11891  lemininf  11912  ltmininf  11913  xrmaxltsup  11936  xrmaxaddlem  11938  xrmaxadd  11939  xrmineqinf  11947  xrltmininf  11948  xrminltinf  11950  xrminadd  11953  climuni  11971  reccn2ap  11991  isumz  12068  geoisum1c  12199  prod1dc  12265  efltim  12377  dvdsval2  12469  dvdscmulr  12499  dvdsmulcr  12500  modmulconst  12502  dvdsadd2b  12519  dvdsexp  12540  mulmoddvds  12542  divalglemeuneg  12602  gcdaddm  12673  dvdsgcdb  12702  mulgcd  12705  gcddiv  12708  uzwodc  12726  lcmdvdsb  12774  mulgcddvds  12784  qredeq  12786  divgcdcoprm0  12791  cncongr1  12793  euclemma  12836  rpexp  12843  rpexp12i  12845  fermltl  12924  prmdiv  12925  odzcllem  12933  odzdvds  12936  odzphi  12937  vfermltl  12942  coprimeprodsq  12948  pythagtriplem6  12961  pythagtriplem7  12962  pythagtriplem12  12966  pythagtriplem13  12967  pceu  12986  pcdvdsb  13011  pcgcd1  13019  dvdsprmpweq  13026  sumhashdc  13038  ctinf  13170  fvsetsid  13235  ressressg  13277  ressabsg  13278  rngplusgg  13339  imasaddvallemg  13517  qusaddvallemg  13535  plusfvalg  13565  mgmb1mgm1  13570  issubmnd  13644  ress0g  13645  imasmnd2  13654  imasmnd  13655  gsumfzz  13697  grpasscan2  13766  grpidrcan  13767  grpidlcan  13768  grpinvadd  13780  grpsubeq0  13788  grppncan  13793  dfgrp3mlem  13800  dfgrp3me  13802  grpsubpropd2  13807  pwsinvg  13814  imasgrp2  13816  imasgrp  13817  mhmmnd  13822  mulgnn0p1  13839  mulgnnsubcl  13840  mulgnn0subcl  13841  mulgsubcl  13842  mulgneg  13846  mulgaddcom  13852  mulginvcom  13853  submmulg  13872  subgcl  13890  subgsubcl  13891  subgsub  13892  subgmulg  13894  nsgconj  13912  nsgid  13921  quseccl0g  13937  ghmmulg  13962  ghmeqker  13977  f1ghm0to0  13978  kerf1ghm  13980  ablinvadd  14016  ablsub4  14019  ablpncan2  14022  subgabl  14038  gsumfzconst  14047  rngcl  14077  imasrng  14089  srgcl  14103  ringcl  14146  crngcom  14147  ringidss  14162  ringcom  14164  imasring  14197  opprringbg  14213  unitmulcl  14247  unitmulclb  14248  dvrcl  14269  unitdvcl  14270  dvrcan1  14274  dvrcan3  14275  rhmmul  14298  subrngrng  14336  subrngmcl  14343  subrgmcl  14367  subrgdv  14372  rrgeq0  14399  domneq0  14407  islmod  14426  scafvalg  14442  lmodcom  14468  rmodislmodlem  14485  rmodislmod  14486  lssclg  14499  lssvnegcl  14511  lssintclm  14519  lspss  14534  lspun  14537  lspsnvsi  14553  rspssp  14629  rnglidlmmgm  14631  rnglidlmsgrp  14632  rnglidlrng  14633  zndvds  14784  psrbaglecl  14811  psrbagcon  14813  2basgeng  14934  iuncld  14967  ntrss  14971  restco  15026  restabs  15027  cnprcl2k  15058  lmconst  15068  cnrest2  15088  cnmpt2t  15145  psmetsym  15181  psmetge0  15183  xmetge0  15217  xmetsym  15220  blvalps  15240  blval  15241  xblcntrps  15265  xblcntr  15266  xmssym  15321  blsscls2  15345  bdxmet  15353  txmetcnp  15370  dvfvalap  15533  dvid  15547  dvidre  15549  dvcnp2cntop  15551  elplyr  15592  rpcxpadd  15757  rpcxpsub  15760  rpmulcxp  15761  rpdivcxp  15763  cxpmul  15764  rpcxple2  15770  rpcxplt2  15771  rplogbval  15797  rplogbcl  15798  rplogbreexp  15805  relogbexpap  15810  logbleb  15813  logblt  15814  rplogbcxp  15815  rpcxplogb  15816  relogbcxpbap  15817  sgmppw  15847  lgsneg1  15885  lgsmod  15886  lgsne0  15898  lgssq  15900  lgsdirnn0  15907  lgsdinn0  15908  lgsquad  15940  funvtxvalg  16018  funiedgvalg  16019  lpvtx  16061  ausgrumgrien  16152  ausgrusgrien  16153  uhgrissubgr  16243  egrsubgr  16245  subumgredg2en  16253  subusgr  16257  wlkl1loop  16340  clwwlknonex2  16421  eulerpathprum  16462  eulerpathum  16463  findset  16702  repiecele0  16797  repiecege0  16798  gfsumsn  16853