Theorem simpr1 1034

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

Assertion

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

Proof of Theorem simpr1

Step	Hyp	Ref	Expression
1		simp1 1028	. 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:  simplr1  1070  simprr1  1076  simp1r1  1124  simp2r1  1130  simp3r1  1136  3anandis  1388  isopolem  6028  caovlem2d  6282  suppfnss  6497  tfrlemibacc  6597  tfrlemibfn  6599  tfr1onlembacc  6613  tfr1onlembfn  6615  tfrcllembacc  6626  tfrcllembfn  6628  eqsupti  7336  prmuloc2  7934  ltntri  8454  elioc2  10340  elico2  10341  elicc2  10342  fseq1p1m1  10503  elfz0ubfz0  10534  ico0  10698  seq3f1olemp  10954  seq3f1oleml  10955  bcval5  11203  hashtpgim  11299  swrdsbslen  11440  ccatswrd  11444  isumss2  12162  tanaddap  12508  dvds2ln  12593  divalglemeunn  12690  divalglemex  12691  divalglemeuneg  12692  qredeq  12876  pcdvdstr  13108  isstructr  13369  imasmnd2  13761  mndissubm  13784  grpsubrcan  13888  grpsubadd  13895  grpsubsub  13896  grpaddsubass  13897  grpsubsub4  13900  grpnnncan2  13904  imasgrp2  13915  mulgnndir  13956  mulgnn0dir  13957  mulgdir  13959  mulgnnass  13962  mulgnn0ass  13963  mulgass  13964  mulgsubdir  13967  issubg2m  13994  eqgval  14028  qusgrp  14037  kerf1ghm  14079  cmn32  14109  cmn12  14111  abladdsub  14121  prdssgrpd  14193  prdsmndd  14196  rngass  14240  imasrng  14257  srgass  14277  ringdilem  14318  ringass  14322  imasring  14371  opprrng  14384  opprring  14386  mulgass3  14393  unitgrp  14425  dvrass  14448  dvrdir  14452  subrgunit  14549  issubrg2  14551  aprap  14600  islss3  14718  sralmod  14789  icnpimaex  15314  cnptopresti  15341  upxp  15375  psmettri  15433  isxmet2d  15451  xmettri  15475  metrtri  15480  xmetres2  15482  bldisj  15504  blss2ps  15509  blss2  15510  xmstri2  15573  mstri2  15574  xmstri  15575  mstri  15576  xmstri3  15577  mstri3  15578  msrtri  15579  comet  15602  bdbl  15606  xmetxp  15610  dvconst  15797  dvconstre  15799  dvconstss  15801  sgmmul  16116  findset  16983  pw1ndom3  17032