Theorem simpr2 1035

Description: Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)

Assertion

Ref	Expression
simpr2	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜒)

Proof of Theorem simpr2

Step	Hyp	Ref	Expression
1		simp2 1029	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜒)
2	1	adantl 277	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜒)

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

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

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

This theorem is used by:  simplr2  1071  simprr2  1077  simp1r2  1125  simp2r2  1131  simp3r2  1137  3anandis  1388  isopolem  6031  tfrlemibacc  6601  tfrlemibfn  6603  tfr1onlembacc  6617  tfr1onlembfn  6619  tfrcllembacc  6630  tfrcllembfn  6632  prltlu  7861  prdisj  7866  prmuloc2  7941  ltntri  8462  eluzuzle  9947  xlesubadd  10303  elioc2  10356  elico2  10357  elicc2  10358  fseq1p1m1  10519  fz0fzelfz0  10552  seq3f1olemp  10974  bcval5  11224  hashdifpr  11284  hashtpgim  11320  swrdsbslen  11461  ccatswrd  11465  swrdswrdlem  11499  summodclem2  12175  isumss2  12186  tanaddap  12532  dvds2ln  12617  divalglemeunn  12714  divalglemex  12715  divalglemeuneg  12716  isstructr  13426  f1ovscpbl  13693  mndissubm  13842  grpsubrcan  13946  grpsubadd  13953  grpaddsubass  13955  grpsubsub4  13958  grppnpcan2  13959  grpnpncan  13960  mulgnndir  14014  mulgnn0dir  14015  mulgdir  14017  mulgnnass  14020  mulgnn0ass  14021  mulgass  14022  mulgsubdir  14025  issubg2m  14052  eqgval  14086  qusgrp  14095  cmn32  14198  cmn12  14200  abladdsub  14210  ablsubsub23  14220  prdssgrpd  14299  prdsmndd  14302  rngass  14346  srgdilem  14381  srgass  14383  ringdilem  14424  ringass  14428  opprrng  14492  opprring  14494  mulgass3  14501  unitgrp  14533  dvrass  14556  dvrdir  14560  subrgunit  14657  issubrg2  14659  aprap  14708  lsssn0  14817  islss3  14826  sralmod  14897  psrringfi  15209  restopnb  15419  icnpimaex  15449  cnptopresti  15476  psmettri  15568  isxmet2d  15586  xmettri  15610  metrtri  15615  xmetres2  15617  bldisj  15639  blss2ps  15644  blss2  15645  xmstri2  15708  mstri2  15709  xmstri  15710  mstri  15711  xmstri3  15712  mstri3  15713  msrtri  15714  comet  15737  bdbl  15741  xmetxp  15745  dvconst  15932  dvconstre  15934  dvconstss  15936  sgmmul  16302  gausslemma2dlem1a  16394  pw1ndom3  17237