Theorem simpr1 1003

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

Assertion

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

Proof of Theorem simpr1

Step	Hyp	Ref	Expression
1		simp1 997	. 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:  simplr1  1039  simprr1  1045  simp1r1  1093  simp2r1  1099  simp3r1  1105  3anandis  1347  isopolem  5822  caovlem2d  6066  tfrlemibacc  6326  tfrlemibfn  6328  tfr1onlembacc  6342  tfr1onlembfn  6344  tfrcllembacc  6355  tfrcllembfn  6357  eqsupti  6994  prmuloc2  7565  ltntri  8084  elioc2  9935  elico2  9936  elicc2  9937  fseq1p1m1  10093  elfz0ubfz0  10124  ico0  10261  seq3f1olemp  10501  seq3f1oleml  10502  bcval5  10742  isumss2  11400  tanaddap  11746  dvds2ln  11830  divalglemeunn  11925  divalglemex  11926  divalglemeuneg  11927  qredeq  12095  pcdvdstr  12325  isstructr  12476  mndissubm  12865  grpsubrcan  12950  grpsubadd  12957  grpsubsub  12958  grpaddsubass  12959  grpsubsub4  12962  grpnnncan2  12966  mulgnndir  13010  mulgnn0dir  13011  mulgdir  13013  mulgnnass  13016  mulgnn0ass  13017  mulgass  13018  mulgsubdir  13021  issubg2m  13047  eqgval  13080  cmn32  13105  cmn12  13107  abladdsub  13116  srgass  13152  ringdilem  13193  ringass  13197  opprring  13247  mulgass3  13252  unitgrp  13283  dvrass  13306  dvrdir  13310  aprap  13342  subrgunit  13365  issubrg2  13367  icnpimaex  13647  cnptopresti  13674  upxp  13708  psmettri  13766  isxmet2d  13784  xmettri  13808  metrtri  13813  xmetres2  13815  bldisj  13837  blss2ps  13842  blss2  13843  xmstri2  13906  mstri2  13907  xmstri  13908  mstri  13909  xmstri3  13910  mstri3  13911  msrtri  13912  comet  13935  bdbl  13939  xmetxp  13943  dvconst  14097  findset  14633