Theorem simp2 1029

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  simpl2  1032  simpr2  1035  simp2i  1038  simp2d  1041  simp12  1059  simp22  1062  simp32  1065  syld3an3  1323  3ianorr  1350  intn3an2d  1398  stoic4b  1482  nlim0  4541  tfisi  4736  sotri2  5188  sotri3  5189  feq123  5528  sefvex  5719  fvmptt  5800  fnfvima  5956  cocan1  5996  cocan2  5997  ovexg  6122  ovmpox  6220  ovmpoga  6221  fvmpopr2d  6228  caovimo  6286  suppval1  6483  suppimacnvfn  6490  suppfnss  6501  tfr1onlembxssdm  6618  tfr1onlembfn  6619  tfrcllembxssdm  6631  tfrcllembfn  6632  freccllem  6677  frecfcllem  6679  frecsuclem  6681  frecrdg  6683  mapm  6974  domssr  7069  mapxpen  7153  dif1en  7188  diffifi  7203  unsnfidcex  7232  unfidisj  7234  undifdc  7236  resfnfinfinss  7258  funrnfi  7261  fissfi  7268  sbthlemi9  7288  elfir  7313  difinfsn  7447  ctssdc  7460  djuassen  7580  xpdjuen  7581  mulcanenq  7759  ltanqg  7774  mulcanenq0ec  7819  addnnnq0  7823  distrprg  7962  aptipr  8015  addsrpr  8119  mulsrpr  8120  mulasssrg  8132  ltpsrprg  8177  axmulass  8247  axpre-ltadd  8260  subadd2  8538  nppcan  8556  nppcan3  8558  subsub2  8562  subsub4  8567  npncan3  8572  pnpcan  8573  pnncan  8575  subcan  8589  ltadd1  8765  leadd1  8766  leadd2  8767  ltsubadd  8768  ltsubadd2  8769  lesubadd  8770  lesubadd2  8771  ltaddsub  8772  leaddsub  8774  lesub1  8792  lesub2  8793  ltsub1  8794  ltsub2  8795  gt0add  8910  apreap  8924  lemul1  8930  reapmul1lem  8931  reapmul1  8932  reapadd1  8933  remulext1  8936  remulext2  8937  apadd2  8946  mulext2  8950  mulap0r  8952  leltap  8962  ltap  8970  apsub1  8979  recexaplem2  8989  mulcanap  9002  mulcanap2  9003  divvalap  9013  divmulap  9014  divcanap1  9020  diveqap0  9021  divap0b  9022  divrecap  9027  divassap  9029  div23ap  9030  divdirap  9036  divcanap3  9037  div11ap  9039  diveqap1  9044  divmuldivap  9051  divcanap5  9053  redivclap  9070  div2negap  9074  apmul1  9127  apmul2  9128  div2subap  9176  ltdiv1  9207  ledivmul  9216  lemuldiv  9220  lt2msq1  9224  ltdiv23  9231  squeeze0  9243  ofsubeq0  9301  ofnegsub  9302  ind1  9310  zaddcllemneg  9695  zfidc  9735  eluzsub  9969  nn01to3  10034  rpgecl  10101  addlelt  10187  xleadd1  10295  xltadd1  10296  lbioog  10333  ubioc1  10349  ubicc2  10405  icoshftf1o  10411  fzen  10465  nelfzo  10577  ubmelfzo  10636  ssfzo12  10660  ubmelm1fzo  10662  fzosplitprm1  10671  zsupssdc  10691  rebtwn2zlemshrink  10706  qbtwnre  10709  icogelb  10718  flqwordi  10745  flqword2  10746  flltdivnn0lt  10761  modqcl  10785  mulqmod0  10789  modqmulnn  10801  modqabs2  10817  modqmuladdnn0  10827  qnegmod  10828  addmodid  10831  modqm1p1mod0  10834  modifeq2int  10845  modqdi  10851  modqeqmodmin  10853  modfzo0difsn  10854  frec2uzf1od  10865  exp3val  11000  expnegap0  11006  expgt1  11036  exprecap  11039  expmulzap  11044  leexp2a  11051  expubnd  11055  mulbinom2  11115  bernneq2  11121  expnbnd  11123  fihashss  11280  fihashssdif  11282  fimaxq  11293  ccatval2  11389  ccatass  11399  ccatw2s1leng  11429  ccat2s1fvwd  11438  swrdval  11443  swrdnd  11454  pfxfv  11479  pfxpfx  11503  ccats1pfxeq  11509  ccats1pfxeqrex  11510  s3cl  11581  s3fv0g  11586  s3fv1g  11587  s3fv2g  11588  shftuz  11605  shftfibg  11608  cjdivap  11698  resqrtcl  11818  absdivap  11859  abssubne0  11881  maxleast  12003  lemininf  12025  ltmininf  12026  xrmaxltsup  12050  xrmaxaddlem  12052  xrmaxadd  12053  xrmineqinf  12061  xrltmininf  12062  xrminltinf  12064  xrminadd  12067  climuni  12085  reccn2ap  12105  isumz  12182  geoisum1c  12313  prod1dc  12379  efltim  12491  dvdsval2  12583  dvdscmulr  12613  dvdsmulcr  12614  modmulconst  12616  dvdsadd2b  12633  dvdsexp  12654  mulmoddvds  12656  divalglemeuneg  12716  gcdaddm  12787  dvdsgcdb  12816  mulgcd  12819  gcddiv  12822  uzwodc  12840  lcmdvdsb  12888  mulgcddvds  12898  qredeq  12900  divgcdcoprm0  12905  cncongr1  12907  euclemma  12951  rpexp  12958  rpexp12i  12960  fermltl  13042  prmdiv  13043  odzcllem  13051  odzdvds  13054  odzphi  13055  vfermltl  13060  coprimeprodsq  13066  pythagtriplem6  13079  pythagtriplem7  13080  pythagtriplem12  13084  pythagtriplem13  13085  pceu  13104  pcdvdsb  13129  pcgcd1  13137  dvdsprmpweq  13144  sumhashdc  13156  ctinf  13380  fvsetsid  13445  ressressg  13489  ressabsg  13490  rngplusgg  13551  imasaddvallemg  13696  qusaddvallemg  13714  plusfvalg  13743  mgmb1mgm1  13748  issubmnd  13815  ress0g  13816  imasmnd2  13819  imasmnd  13820  grpasscan2  13929  grpidrcan  13930  grpidlcan  13931  grpinvadd  13943  grpsubeq0  13951  grppncan  13956  dfgrp3mlem  13963  dfgrp3me  13965  grpsubpropd2  13970  imasgrp2  13973  imasgrp  13974  mhmmnd  13979  mulgnn0p1  13996  mulgnnsubcl  13997  mulgnn0subcl  13998  mulgsubcl  13999  mulgneg  14003  mulgaddcom  14009  mulginvcom  14010  submmulg  14029  subgcl  14047  subgsubcl  14048  subgsub  14049  subgmulg  14051  nsgconj  14069  nsgid  14078  quseccl0g  14094  ghmmulg  14119  ghmeqker  14134  f1ghm0to0  14135  kerf1ghm  14137  ablinvadd  14205  ablsub4  14208  ablpncan2  14211  subgabl  14227  gzsumconst  14234  gsumsncmn  14247  gsumconstcmn  14267  pwsinvg  14323  rngcl  14351  imasrng  14363  srgcl  14382  ringcl  14425  crngcom  14426  ringidss  14442  ringcom  14444  imasring  14479  opprringbg  14495  unitmulcl  14530  unitmulclb  14531  dvrcl  14552  unitdvcl  14553  dvrcan1  14557  dvrcan3  14558  rhmmul  14581  subrngrng  14620  subrngmcl  14627  subrgmcl  14651  subrgdv  14656  rrgeq0  14683  domneq0  14691  islmod  14737  scafvalg  14754  lmodcom  14780  rmodislmodlem  14797  rmodislmod  14798  lssclg  14811  lssvnegcl  14823  lssintclm  14831  lspss  14846  lspun  14849  lspsnvsi  14865  rspssp  14941  rnglidlmmgm  14943  rnglidlmsgrp  14944  rnglidlrng  14945  zndvds  15094  aspss  15129  asclmul1  15139  asclmul2  15140  ascldimul  15141  asclinvg  15142  asclmulg  15154  psrbagdceq  15169  psrbaglecl  15174  psrbagcon  15176  psrringfi  15209  2basgeng  15320  iuncld  15353  ntrss  15357  restco  15412  restabs  15413  cnprcl2k  15444  lmconst  15454  cnrest2  15474  cnmpt2t  15531  psmetsym  15567  psmetge0  15569  xmetge0  15603  xmetsym  15606  blvalps  15626  blval  15627  xblcntrps  15651  xblcntr  15652  xmssym  15707  blsscls2  15731  bdxmet  15739  txmetcnp  15756  dvfvalap  15919  dvid  15933  dvidre  15935  dvcnp2cntop  15937  elplyr  15978  logfac  16138  rpcxpadd  16150  rpcxpsub  16153  rpmulcxp  16154  rpdivcxp  16156  cxpmul  16157  rpcxple2  16165  rpcxplt2  16166  rplogbval  16193  rplogbcl  16194  rplogbreexp  16201  relogbexpap  16206  logbleb  16209  logblt  16210  rplogbcxp  16211  rpcxplogb  16212  relogbcxpbap  16213  sgmppw  16298  bcmono  16316  prmefexple  16320  lgsneg1  16361  lgsmod  16362  lgsne0  16374  lgssq  16376  lgsdirnn0  16383  lgsdinn0  16384  lgsquad  16416  funvtxvalg  16494  funiedgvalg  16495  lpvtx  16537  ausgrumgrien  16628  ausgrusgrien  16629  uhgrissubgr  16719  egrsubgr  16721  subumgredg2en  16729  subusgr  16733  wlkl1loop  16816  clwwlknonex2  16897  eulerpathprum  16938  eulerpathum  16939  findset  17188  repiecele0  17293  repiecege0  17294