Theorem simpr1 988

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

Assertion

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

Proof of Theorem simpr1

Step	Hyp	Ref	Expression
1		simp1 982	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜓)
2	1	adantl 275	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 963

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

This theorem depends on definitions:  df-bi 116  df-3an 965

This theorem is referenced by:  simplr1  1024  simprr1  1030  simp1r1  1078  simp2r1  1084  simp3r1  1090  3anandis  1329  isopolem  5767  caovlem2d  6007  tfrlemibacc  6267  tfrlemibfn  6269  tfr1onlembacc  6283  tfr1onlembfn  6285  tfrcllembacc  6296  tfrcllembfn  6298  eqsupti  6932  prmuloc2  7470  ltntri  7986  elioc2  9822  elico2  9823  elicc2  9824  fseq1p1m1  9978  elfz0ubfz0  10006  ico0  10143  seq3f1olemp  10383  seq3f1oleml  10384  bcval5  10619  isumss2  11272  tanaddap  11618  dvds2ln  11701  divalglemeunn  11793  divalglemex  11794  divalglemeuneg  11795  qredeq  11953  isstructr  12165  icnpimaex  12571  cnptopresti  12598  upxp  12632  psmettri  12690  isxmet2d  12708  xmettri  12732  metrtri  12737  xmetres2  12739  bldisj  12761  blss2ps  12766  blss2  12767  xmstri2  12830  mstri2  12831  xmstri  12832  mstri  12833  xmstri3  12834  mstri3  12835  msrtri  12836  comet  12859  bdbl  12863  xmetxp  12867  dvconst  13021  findset  13479