Theorem simpr1 1030

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

Assertion

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

Proof of Theorem simpr1

Step	Hyp	Ref	Expression
1		simp1 1024	. 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:  simplr1  1066  simprr1  1072  simp1r1  1120  simp2r1  1126  simp3r1  1132  3anandis  1384  isopolem  6002  caovlem2d  6256  suppfnss  6471  tfrlemibacc  6571  tfrlemibfn  6573  tfr1onlembacc  6587  tfr1onlembfn  6589  tfrcllembacc  6600  tfrcllembfn  6602  eqsupti  7301  prmuloc2  7899  ltntri  8419  elioc2  10292  elico2  10293  elicc2  10294  fseq1p1m1  10454  elfz0ubfz0  10485  ico0  10649  seq3f1olemp  10905  seq3f1oleml  10906  bcval5  11154  hashtpgim  11246  swrdsbslen  11387  ccatswrd  11391  isumss2  12109  tanaddap  12455  dvds2ln  12540  divalglemeunn  12637  divalglemex  12638  divalglemeuneg  12639  qredeq  12823  pcdvdstr  13055  isstructr  13316  imasmnd2  13712  mndissubm  13735  grpsubrcan  13841  grpsubadd  13848  grpsubsub  13849  grpaddsubass  13850  grpsubsub4  13853  grpnnncan2  13857  imasgrp2  13868  mulgnndir  13909  mulgnn0dir  13910  mulgdir  13912  mulgnnass  13915  mulgnn0ass  13916  mulgass  13917  mulgsubdir  13920  issubg2m  13947  eqgval  13981  qusgrp  13990  kerf1ghm  14032  cmn32  14062  cmn12  14064  abladdsub  14073  prdssgrpd  14138  prdsmndd  14141  rngass  14183  imasrng  14200  srgass  14219  ringdilem  14260  ringass  14264  imasring  14312  opprrng  14325  opprring  14327  mulgass3  14334  unitgrp  14366  dvrass  14389  dvrdir  14393  subrgunit  14490  issubrg2  14492  aprap  14541  islss3  14658  sralmod  14729  icnpimaex  15207  cnptopresti  15234  upxp  15268  psmettri  15326  isxmet2d  15344  xmettri  15368  metrtri  15373  xmetres2  15375  bldisj  15397  blss2ps  15402  blss2  15403  xmstri2  15466  mstri2  15467  xmstri  15468  mstri  15469  xmstri3  15470  mstri3  15471  msrtri  15472  comet  15495  bdbl  15499  xmetxp  15503  dvconst  15690  dvconstre  15692  dvconstss  15694  sgmmul  15995  findset  16856  pw1ndom3  16905