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  4491  tfisi  4685  sotri2  5134  sotri3  5135  feq123  5474  sefvex  5660  fvmptt  5738  fnfvima  5889  cocan1  5928  cocan2  5929  ovexg  6052  ovmpox  6150  ovmpoga  6151  fvmpopr2d  6158  caovimo  6216  tfr1onlembxssdm  6509  tfr1onlembfn  6510  tfrcllembxssdm  6522  tfrcllembfn  6523  freccllem  6568  frecfcllem  6570  frecsuclem  6572  frecrdg  6574  domssr  6951  mapxpen  7034  dif1en  7068  diffifi  7083  unsnfidcex  7112  unfidisj  7114  undifdc  7116  resfnfinfinss  7138  funrnfi  7141  sbthlemi9  7164  elfir  7172  difinfsn  7299  ctssdc  7312  djuassen  7432  xpdjuen  7433  mulcanenq  7605  ltanqg  7620  mulcanenq0ec  7665  addnnnq0  7669  distrprg  7808  aptipr  7861  addsrpr  7965  mulsrpr  7966  mulasssrg  7978  ltpsrprg  8023  axmulass  8093  axpre-ltadd  8106  subadd2  8383  nppcan  8401  nppcan3  8403  subsub2  8407  subsub4  8412  npncan3  8417  pnpcan  8418  pnncan  8420  subcan  8434  ltadd1  8609  leadd1  8610  leadd2  8611  ltsubadd  8612  ltsubadd2  8613  lesubadd  8614  lesubadd2  8615  ltaddsub  8616  leaddsub  8618  lesub1  8636  lesub2  8637  ltsub1  8638  ltsub2  8639  gt0add  8753  apreap  8767  lemul1  8773  reapmul1lem  8774  reapmul1  8775  reapadd1  8776  remulext1  8779  remulext2  8780  apadd2  8789  mulext2  8793  mulap0r  8795  leltap  8805  ltap  8813  apsub1  8822  recexaplem2  8832  mulcanap  8845  mulcanap2  8846  divvalap  8854  divmulap  8855  divcanap1  8861  diveqap0  8862  divap0b  8863  divrecap  8868  divassap  8870  div23ap  8871  divdirap  8877  divcanap3  8878  div11ap  8880  diveqap1  8885  divmuldivap  8892  divcanap5  8894  redivclap  8911  div2negap  8915  apmul1  8968  apmul2  8969  div2subap  9017  ltdiv1  9048  ledivmul  9057  lemuldiv  9061  lt2msq1  9065  ltdiv23  9072  squeeze0  9084  ofnegsub  9142  zaddcllemneg  9518  eluzsub  9786  nn01to3  9851  rpgecl  9917  addlelt  10003  xleadd1  10110  xltadd1  10111  lbioog  10148  ubioc1  10164  ubicc2  10220  icoshftf1o  10226  fzen  10278  nelfzo  10387  ubmelfzo  10446  ssfzo12  10470  ubmelm1fzo  10472  fzosplitprm1  10481  zsupssdc  10499  rebtwn2zlemshrink  10514  qbtwnre  10517  icogelb  10526  flqwordi  10549  flqword2  10550  flltdivnn0lt  10565  modqcl  10589  mulqmod0  10593  modqmulnn  10605  modqabs2  10621  modqmuladdnn0  10631  qnegmod  10632  addmodid  10635  modqm1p1mod0  10638  modifeq2int  10649  modqdi  10655  modqeqmodmin  10657  modfzo0difsn  10658  frec2uzf1od  10669  exp3val  10804  expnegap0  10810  expgt1  10840  exprecap  10843  expmulzap  10848  leexp2a  10855  expubnd  10859  mulbinom2  10919  bernneq2  10924  expnbnd  10926  fihashss  11081  fihashssdif  11083  fimaxq  11092  ccatval2  11176  ccatass  11186  ccatw2s1leng  11216  ccat2s1fvwd  11225  swrdval  11230  swrdnd  11241  pfxfv  11266  pfxpfx  11290  ccats1pfxeq  11296  ccats1pfxeqrex  11297  s3cl  11368  s3fv0g  11373  s3fv1g  11374  s3fv2g  11375  shftuz  11379  shftfibg  11382  cjdivap  11471  resqrtcl  11591  absdivap  11632  abssubne0  11653  maxleast  11775  lemininf  11796  ltmininf  11797  xrmaxltsup  11820  xrmaxaddlem  11822  xrmaxadd  11823  xrmineqinf  11831  xrltmininf  11832  xrminltinf  11834  xrminadd  11837  climuni  11855  reccn2ap  11875  isumz  11952  geoisum1c  12083  prod1dc  12149  efltim  12261  dvdsval2  12353  dvdscmulr  12383  dvdsmulcr  12384  modmulconst  12386  dvdsadd2b  12403  dvdsexp  12424  mulmoddvds  12426  divalglemeuneg  12486  gcdaddm  12557  dvdsgcdb  12586  mulgcd  12589  gcddiv  12592  uzwodc  12610  lcmdvdsb  12658  mulgcddvds  12668  qredeq  12670  divgcdcoprm0  12675  cncongr1  12677  euclemma  12720  rpexp  12727  rpexp12i  12729  fermltl  12808  prmdiv  12809  odzcllem  12817  odzdvds  12820  odzphi  12821  vfermltl  12826  coprimeprodsq  12832  pythagtriplem6  12845  pythagtriplem7  12846  pythagtriplem12  12850  pythagtriplem13  12851  pceu  12870  pcdvdsb  12895  pcgcd1  12903  dvdsprmpweq  12910  sumhashdc  12922  ctinf  13053  fvsetsid  13118  ressressg  13160  ressabsg  13161  rngplusgg  13222  imasaddvallemg  13400  qusaddvallemg  13418  plusfvalg  13448  mgmb1mgm1  13453  issubmnd  13527  ress0g  13528  imasmnd2  13537  imasmnd  13538  gsumfzz  13580  grpasscan2  13649  grpidrcan  13650  grpidlcan  13651  grpinvadd  13663  grpsubeq0  13671  grppncan  13676  dfgrp3mlem  13683  dfgrp3me  13685  grpsubpropd2  13690  pwsinvg  13697  imasgrp2  13699  imasgrp  13700  mhmmnd  13705  mulgnn0p1  13722  mulgnnsubcl  13723  mulgnn0subcl  13724  mulgsubcl  13725  mulgneg  13729  mulgaddcom  13735  mulginvcom  13736  submmulg  13755  subgcl  13773  subgsubcl  13774  subgsub  13775  subgmulg  13777  nsgconj  13795  nsgid  13804  quseccl0g  13820  ghmmulg  13845  ghmeqker  13860  f1ghm0to0  13861  kerf1ghm  13863  ablinvadd  13899  ablsub4  13902  ablpncan2  13905  subgabl  13921  gsumfzconst  13930  rngcl  13960  imasrng  13972  srgcl  13986  ringcl  14029  crngcom  14030  ringidss  14045  ringcom  14047  imasring  14080  opprringbg  14096  unitmulcl  14130  unitmulclb  14131  dvrcl  14152  unitdvcl  14153  dvrcan1  14157  dvrcan3  14158  rhmmul  14181  subrngrng  14219  subrngmcl  14226  subrgmcl  14250  subrgdv  14255  rrgeq0  14282  domneq0  14289  islmod  14308  scafvalg  14324  lmodcom  14350  rmodislmodlem  14367  rmodislmod  14368  lssclg  14381  lssvnegcl  14393  lssintclm  14401  lspss  14416  lspun  14419  lspsnvsi  14435  rspssp  14511  rnglidlmmgm  14513  rnglidlmsgrp  14514  rnglidlrng  14515  zndvds  14666  2basgeng  14809  iuncld  14842  ntrss  14846  restco  14901  restabs  14902  cnprcl2k  14933  lmconst  14943  cnrest2  14963  cnmpt2t  15020  psmetsym  15056  psmetge0  15058  xmetge0  15092  xmetsym  15095  blvalps  15115  blval  15116  xblcntrps  15140  xblcntr  15141  xmssym  15196  blsscls2  15220  bdxmet  15228  txmetcnp  15245  dvfvalap  15408  dvid  15422  dvidre  15424  dvcnp2cntop  15426  elplyr  15467  rpcxpadd  15632  rpcxpsub  15635  rpmulcxp  15636  rpdivcxp  15638  cxpmul  15639  rpcxple2  15645  rpcxplt2  15646  rplogbval  15672  rplogbcl  15673  rplogbreexp  15680  relogbexpap  15685  logbleb  15688  logblt  15689  rplogbcxp  15690  rpcxplogb  15691  relogbcxpbap  15692  sgmppw  15719  lgsneg1  15757  lgsmod  15758  lgsne0  15770  lgssq  15772  lgsdirnn0  15779  lgsdinn0  15780  lgsquad  15812  funvtxvalg  15890  funiedgvalg  15891  lpvtx  15933  ausgrumgrien  16024  ausgrusgrien  16025  uhgrissubgr  16115  egrsubgr  16117  subumgredg2en  16125  subusgr  16129  wlkl1loop  16212  clwwlknonex2  16293  findset  16561  gfsumsn  16706