Theorem simpr2 1031

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

Assertion

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

Proof of Theorem simpr2

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

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 1005

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

This theorem depends on definitions:  df-bi 117  df-3an 1007

This theorem is referenced by:  simplr2  1067  simprr2  1073  simp1r2  1121  simp2r2  1127  simp3r2  1133  3anandis  1384  isopolem  6001  tfrlemibacc  6570  tfrlemibfn  6572  tfr1onlembacc  6586  tfr1onlembfn  6588  tfrcllembacc  6599  tfrcllembfn  6601  prltlu  7818  prdisj  7823  prmuloc2  7898  ltntri  8418  eluzuzle  9883  xlesubadd  10238  elioc2  10291  elico2  10292  elicc2  10293  fseq1p1m1  10453  fz0fzelfz0  10486  seq3f1olemp  10904  bcval5  11153  hashdifpr  11213  hashtpgim  11245  swrdsbslen  11386  ccatswrd  11390  swrdswrdlem  11424  summodclem2  12096  isumss2  12107  tanaddap  12453  dvds2ln  12538  divalglemeunn  12635  divalglemex  12636  divalglemeuneg  12637  isstructr  13314  f1ovscpbl  13579  mndissubm  13733  grpsubrcan  13839  grpsubadd  13846  grpaddsubass  13848  grpsubsub4  13851  grppnpcan2  13852  grpnpncan  13853  mulgnndir  13907  mulgnn0dir  13908  mulgdir  13910  mulgnnass  13913  mulgnn0ass  13914  mulgass  13915  mulgsubdir  13918  issubg2m  13945  eqgval  13979  qusgrp  13988  cmn32  14060  cmn12  14062  abladdsub  14071  ablsubsub23  14081  prdssgrpd  14136  prdsmndd  14139  rngass  14181  srgdilem  14215  srgass  14217  ringdilem  14258  ringass  14262  opprrng  14323  opprring  14325  mulgass3  14332  unitgrp  14364  dvrass  14387  dvrdir  14391  subrgunit  14488  issubrg2  14490  aprap  14539  lsssn0  14647  islss3  14656  sralmod  14727  restopnb  15175  icnpimaex  15205  cnptopresti  15232  psmettri  15324  isxmet2d  15342  xmettri  15366  metrtri  15371  xmetres2  15373  bldisj  15395  blss2ps  15400  blss2  15401  xmstri2  15464  mstri2  15465  xmstri  15466  mstri  15467  xmstri3  15468  mstri3  15469  msrtri  15470  comet  15493  bdbl  15497  xmetxp  15501  dvconst  15688  dvconstre  15690  dvconstss  15692  sgmmul  15993  gausslemma2dlem1a  16060  pw1ndom3  16903