Theorem simp3 940

Description: Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)

Assertion

Ref	Expression
simp3	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜒)

Proof of Theorem simp3

Step	Hyp	Ref	Expression
1		3simpc 937	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜒))
2	1	simprd 112	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜒)

Syntax hints:   → wi 4   ∧ w3a 919

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115  df-3an 921

This theorem is referenced by:  simpl3  943  simpr3  946  simp3i  949  simp3d  952  simp13  970  simp23  973  simp33  976  3anibar  1106  3ianorr  1240  stoic4a  1361  stoic4b  1362  mob2  2772  sotri2  4742  sotri3  4743  feq123  5058  resasplitss  5089  sefvex  5216  ftpg  5368  fsnunf  5383  fnfvima  5414  cocan1  5447  cocan2  5448  f1oiso2  5486  riotass  5515  moriotass  5516  ovmpt2x  5649  ovmpt2ga  5650  caovimo  5714  ofrval  5742  dfsmo2  5925  nnsucsssuc  6094  f1oen2g  6258  f1dom2g  6259  xpdom3m  6331  diffifi  6378  mulcanenq  6575  ltanqg  6590  addnnnq0  6639  nnanq0  6648  prltlu  6677  distrprg  6778  ltexprlemm  6790  recexprlem1ssl  6823  recexprlem1ssu  6824  addsrpr  6922  mulsrpr  6923  mulasssrg  6935  recexgt0sr  6950  axmulass  7039  axpre-ltadd  7052  ltxrlt  7178  subadd2  7312  addsubass  7318  nppcan  7330  nppcan3  7332  subcan2  7333  subsub2  7336  subsub4  7341  pnpcan  7347  pnncan  7349  subcan  7363  subdi  7489  ltadd1  7533  leadd1  7534  leadd2  7535  ltsubadd  7536  ltsubadd2  7537  lesubadd  7538  lesubadd2  7539  ltaddsub  7540  leaddsub  7542  lesub1  7560  lesub2  7561  ltsub1  7562  ltsub2  7563  ltaddsublt  7671  gt0add  7673  reapadd1  7696  remulext1  7699  remulext2  7700  apadd2  7709  mulext2  7713  mulap0r  7715  leltap  7724  ltap  7731  divap0b  7771  divmulasscomap  7784  divcanap5  7802  dmdcanap  7810  redivclap  7819  div2negap  7823  lt2msq1  7963  ltdiv2  7965  nndivtr  8080  gtndiv  8442  eluzsub  8648  nn01to3  8702  qdivcl  8728  irrmul  8732  rpgecl  8762  divge1  8800  ubioog  8937  ubioc1  8952  lbico1  8953  iccleub  8954  lbicc2  9006  ubicc2  9007  icoshftf1o  9013  fzen  9062  elfz1b  9107  uznfz  9120  elfzo0  9191  elfzo0z  9193  ubmelfzo  9209  fzonn0p1p1  9222  ubmelm1fzo  9235  qbtwnre  9265  flqwordi  9290  flltdivnn0lt  9306  ceiqle  9315  modqval  9326  modqvalr  9327  modqcl  9328  flqpmodeq  9329  modq0  9331  mulqmod0  9332  negqmod0  9333  modqge0  9334  modqlt  9335  modqdiffl  9337  modqdifz  9338  modqmulnn  9344  modqvalp1  9345  modqabs2  9360  modqmuladdnn0  9370  qnegmod  9371  addmodid  9374  modqeqmodmin  9396  modfzo0difsn  9397  addmodlteq  9400  frec2uzf1od  9408  expnegap0  9484  expgt1  9514  exprecap  9517  expaddzaplem  9519  expaddzap  9520  expmulzap  9522  mulbinom2  9589  expnbnd  9596  shftfibg  9708  redivap  9761  imdivap  9768  cjdivap  9796  maxleast  10099  lemininf  10115  ltmininf  10116  climuni  10132  summodnegmod  10226  dvdsmultr2  10235  mulmoddvds  10263  divalglemeuneg  10323  gcdaddm  10375  gcdass  10404  mulgcd  10405  gcddiv  10408  lcmass  10467  mulgcddvds  10476  qredeq  10478  congr  10482  divgcdcoprmex  10484  cncongr1  10485  cncongr2  10486  prmexpb  10530  rpexp  10532