Theorem simpr2 1004

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

Assertion

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

Proof of Theorem simpr2

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

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

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 980

This theorem is referenced by:  simplr2  1040  simprr2  1046  simp1r2  1094  simp2r2  1100  simp3r2  1106  3anandis  1347  isopolem  5822  tfrlemibacc  6326  tfrlemibfn  6328  tfr1onlembacc  6342  tfr1onlembfn  6344  tfrcllembacc  6355  tfrcllembfn  6357  prltlu  7485  prdisj  7490  prmuloc2  7565  ltntri  8083  eluzuzle  9534  xlesubadd  9881  elioc2  9934  elico2  9935  elicc2  9936  fseq1p1m1  10091  fz0fzelfz0  10124  seq3f1olemp  10499  bcval5  10738  hashdifpr  10795  summodclem2  11385  isumss2  11396  tanaddap  11742  dvds2ln  11826  divalglemeunn  11920  divalglemex  11921  divalglemeuneg  11922  isstructr  12471  f1ovscpbl  12715  mndissubm  12820  grpsubrcan  12905  grpsubadd  12912  grpaddsubass  12914  grpsubsub4  12917  grppnpcan2  12918  grpnpncan  12919  mulgnndir  12965  mulgnn0dir  12966  mulgdir  12968  mulgnnass  12971  mulgnn0ass  12972  mulgass  12973  mulgsubdir  12976  issubg2m  13002  eqgval  13035  cmn32  13060  cmn12  13062  abladdsub  13071  ablsubsub23  13081  srgdilem  13105  srgass  13107  ringdilem  13148  ringass  13152  opprring  13202  mulgass3  13207  unitgrp  13238  dvrass  13261  dvrdir  13265  aprap  13297  subrgunit  13320  issubrg2  13322  restopnb  13574  icnpimaex  13604  cnptopresti  13631  psmettri  13723  isxmet2d  13741  xmettri  13765  metrtri  13770  xmetres2  13772  bldisj  13794  blss2ps  13799  blss2  13800  xmstri2  13863  mstri2  13864  xmstri  13865  mstri  13866  xmstri3  13867  mstri3  13868  msrtri  13869  comet  13892  bdbl  13896  xmetxp  13900  dvconst  14054