Theorem simp2 1024

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

Syntax hints:   → wi 4   ∧ w3a 1004

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 1006

This theorem is referenced by:  simpl2  1027  simpr2  1030  simp2i  1033  simp2d  1036  simp12  1054  simp22  1057  simp32  1060  syld3an3  1318  3ianorr  1345  intn3an2d  1393  stoic4b  1477  nlim0  4493  tfisi  4687  sotri2  5136  sotri3  5137  feq123  5476  sefvex  5663  fvmptt  5741  fnfvima  5894  cocan1  5933  cocan2  5934  ovexg  6057  ovmpox  6155  ovmpoga  6156  fvmpopr2d  6163  caovimo  6221  tfr1onlembxssdm  6514  tfr1onlembfn  6515  tfrcllembxssdm  6527  tfrcllembfn  6528  freccllem  6573  frecfcllem  6575  frecsuclem  6577  frecrdg  6579  domssr  6956  mapxpen  7039  dif1en  7073  diffifi  7088  unsnfidcex  7117  unfidisj  7119  undifdc  7121  resfnfinfinss  7143  funrnfi  7146  sbthlemi9  7169  elfir  7177  difinfsn  7304  ctssdc  7317  djuassen  7437  xpdjuen  7438  mulcanenq  7610  ltanqg  7625  mulcanenq0ec  7670  addnnnq0  7674  distrprg  7813  aptipr  7866  addsrpr  7970  mulsrpr  7971  mulasssrg  7983  ltpsrprg  8028  axmulass  8098  axpre-ltadd  8111  subadd2  8388  nppcan  8406  nppcan3  8408  subsub2  8412  subsub4  8417  npncan3  8422  pnpcan  8423  pnncan  8425  subcan  8439  ltadd1  8614  leadd1  8615  leadd2  8616  ltsubadd  8617  ltsubadd2  8618  lesubadd  8619  lesubadd2  8620  ltaddsub  8621  leaddsub  8623  lesub1  8641  lesub2  8642  ltsub1  8643  ltsub2  8644  gt0add  8758  apreap  8772  lemul1  8778  reapmul1lem  8779  reapmul1  8780  reapadd1  8781  remulext1  8784  remulext2  8785  apadd2  8794  mulext2  8798  mulap0r  8800  leltap  8810  ltap  8818  apsub1  8827  recexaplem2  8837  mulcanap  8850  mulcanap2  8851  divvalap  8859  divmulap  8860  divcanap1  8866  diveqap0  8867  divap0b  8868  divrecap  8873  divassap  8875  div23ap  8876  divdirap  8882  divcanap3  8883  div11ap  8885  diveqap1  8890  divmuldivap  8897  divcanap5  8899  redivclap  8916  div2negap  8920  apmul1  8973  apmul2  8974  div2subap  9022  ltdiv1  9053  ledivmul  9062  lemuldiv  9066  lt2msq1  9070  ltdiv23  9077  squeeze0  9089  ofnegsub  9147  zaddcllemneg  9523  eluzsub  9791  nn01to3  9856  rpgecl  9922  addlelt  10008  xleadd1  10115  xltadd1  10116  lbioog  10153  ubioc1  10169  ubicc2  10225  icoshftf1o  10231  fzen  10283  nelfzo  10392  ubmelfzo  10451  ssfzo12  10475  ubmelm1fzo  10477  fzosplitprm1  10486  zsupssdc  10504  rebtwn2zlemshrink  10519  qbtwnre  10522  icogelb  10531  flqwordi  10554  flqword2  10555  flltdivnn0lt  10570  modqcl  10594  mulqmod0  10598  modqmulnn  10610  modqabs2  10626  modqmuladdnn0  10636  qnegmod  10637  addmodid  10640  modqm1p1mod0  10643  modifeq2int  10654  modqdi  10660  modqeqmodmin  10662  modfzo0difsn  10663  frec2uzf1od  10674  exp3val  10809  expnegap0  10815  expgt1  10845  exprecap  10848  expmulzap  10853  leexp2a  10860  expubnd  10864  mulbinom2  10924  bernneq2  10929  expnbnd  10931  fihashss  11086  fihashssdif  11088  fimaxq  11097  ccatval2  11184  ccatass  11194  ccatw2s1leng  11224  ccat2s1fvwd  11233  swrdval  11238  swrdnd  11249  pfxfv  11274  pfxpfx  11298  ccats1pfxeq  11304  ccats1pfxeqrex  11305  s3cl  11376  s3fv0g  11381  s3fv1g  11382  s3fv2g  11383  shftuz  11400  shftfibg  11403  cjdivap  11492  resqrtcl  11612  absdivap  11653  abssubne0  11674  maxleast  11796  lemininf  11817  ltmininf  11818  xrmaxltsup  11841  xrmaxaddlem  11843  xrmaxadd  11844  xrmineqinf  11852  xrltmininf  11853  xrminltinf  11855  xrminadd  11858  climuni  11876  reccn2ap  11896  isumz  11973  geoisum1c  12104  prod1dc  12170  efltim  12282  dvdsval2  12374  dvdscmulr  12404  dvdsmulcr  12405  modmulconst  12407  dvdsadd2b  12424  dvdsexp  12445  mulmoddvds  12447  divalglemeuneg  12507  gcdaddm  12578  dvdsgcdb  12607  mulgcd  12610  gcddiv  12613  uzwodc  12631  lcmdvdsb  12679  mulgcddvds  12689  qredeq  12691  divgcdcoprm0  12696  cncongr1  12698  euclemma  12741  rpexp  12748  rpexp12i  12750  fermltl  12829  prmdiv  12830  odzcllem  12838  odzdvds  12841  odzphi  12842  vfermltl  12847  coprimeprodsq  12853  pythagtriplem6  12866  pythagtriplem7  12867  pythagtriplem12  12871  pythagtriplem13  12872  pceu  12891  pcdvdsb  12916  pcgcd1  12924  dvdsprmpweq  12931  sumhashdc  12943  ctinf  13074  fvsetsid  13139  ressressg  13181  ressabsg  13182  rngplusgg  13243  imasaddvallemg  13421  qusaddvallemg  13439  plusfvalg  13469  mgmb1mgm1  13474  issubmnd  13548  ress0g  13549  imasmnd2  13558  imasmnd  13559  gsumfzz  13601  grpasscan2  13670  grpidrcan  13671  grpidlcan  13672  grpinvadd  13684  grpsubeq0  13692  grppncan  13697  dfgrp3mlem  13704  dfgrp3me  13706  grpsubpropd2  13711  pwsinvg  13718  imasgrp2  13720  imasgrp  13721  mhmmnd  13726  mulgnn0p1  13743  mulgnnsubcl  13744  mulgnn0subcl  13745  mulgsubcl  13746  mulgneg  13750  mulgaddcom  13756  mulginvcom  13757  submmulg  13776  subgcl  13794  subgsubcl  13795  subgsub  13796  subgmulg  13798  nsgconj  13816  nsgid  13825  quseccl0g  13841  ghmmulg  13866  ghmeqker  13881  f1ghm0to0  13882  kerf1ghm  13884  ablinvadd  13920  ablsub4  13923  ablpncan2  13926  subgabl  13942  gsumfzconst  13951  rngcl  13981  imasrng  13993  srgcl  14007  ringcl  14050  crngcom  14051  ringidss  14066  ringcom  14068  imasring  14101  opprringbg  14117  unitmulcl  14151  unitmulclb  14152  dvrcl  14173  unitdvcl  14174  dvrcan1  14178  dvrcan3  14179  rhmmul  14202  subrngrng  14240  subrngmcl  14247  subrgmcl  14271  subrgdv  14276  rrgeq0  14303  domneq0  14310  islmod  14329  scafvalg  14345  lmodcom  14371  rmodislmodlem  14388  rmodislmod  14389  lssclg  14402  lssvnegcl  14414  lssintclm  14422  lspss  14437  lspun  14440  lspsnvsi  14456  rspssp  14532  rnglidlmmgm  14534  rnglidlmsgrp  14535  rnglidlrng  14536  zndvds  14687  psrbaglecl  14713  psrbagcon  14714  2basgeng  14835  iuncld  14868  ntrss  14872  restco  14927  restabs  14928  cnprcl2k  14959  lmconst  14969  cnrest2  14989  cnmpt2t  15046  psmetsym  15082  psmetge0  15084  xmetge0  15118  xmetsym  15121  blvalps  15141  blval  15142  xblcntrps  15166  xblcntr  15167  xmssym  15222  blsscls2  15246  bdxmet  15254  txmetcnp  15271  dvfvalap  15434  dvid  15448  dvidre  15450  dvcnp2cntop  15452  elplyr  15493  rpcxpadd  15658  rpcxpsub  15661  rpmulcxp  15662  rpdivcxp  15664  cxpmul  15665  rpcxple2  15671  rpcxplt2  15672  rplogbval  15698  rplogbcl  15699  rplogbreexp  15706  relogbexpap  15711  logbleb  15714  logblt  15715  rplogbcxp  15716  rpcxplogb  15717  relogbcxpbap  15718  sgmppw  15745  lgsneg1  15783  lgsmod  15784  lgsne0  15796  lgssq  15798  lgsdirnn0  15805  lgsdinn0  15806  lgsquad  15838  funvtxvalg  15916  funiedgvalg  15917  lpvtx  15959  ausgrumgrien  16050  ausgrusgrien  16051  uhgrissubgr  16141  egrsubgr  16143  subumgredg2en  16151  subusgr  16155  wlkl1loop  16238  clwwlknonex2  16319  eulerpathprum  16360  eulerpathum  16361  findset  16600  repiecele0  16697  repiecege0  16698  gfsumsn  16753