Theorem simpr1 1027

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

Assertion

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

Proof of Theorem simpr1

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

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

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 1004

This theorem is referenced by:  simplr1  1063  simprr1  1069  simp1r1  1117  simp2r1  1123  simp3r1  1129  3anandis  1381  isopolem  5952  caovlem2d  6204  tfrlemibacc  6478  tfrlemibfn  6480  tfr1onlembacc  6494  tfr1onlembfn  6496  tfrcllembacc  6507  tfrcllembfn  6509  eqsupti  7171  prmuloc2  7762  ltntri  8282  elioc2  10140  elico2  10141  elicc2  10142  fseq1p1m1  10298  elfz0ubfz0  10329  ico0  10489  seq3f1olemp  10745  seq3f1oleml  10746  bcval5  10993  swrdsbslen  11206  ccatswrd  11210  isumss2  11912  tanaddap  12258  dvds2ln  12343  divalglemeunn  12440  divalglemex  12441  divalglemeuneg  12442  qredeq  12626  pcdvdstr  12858  isstructr  13055  prdssgrpd  13456  prdsmndd  13489  imasmnd2  13493  mndissubm  13516  grpsubrcan  13622  grpsubadd  13629  grpsubsub  13630  grpaddsubass  13631  grpsubsub4  13634  grpnnncan2  13638  imasgrp2  13655  mulgnndir  13696  mulgnn0dir  13697  mulgdir  13699  mulgnnass  13702  mulgnn0ass  13703  mulgass  13704  mulgsubdir  13707  issubg2m  13734  eqgval  13768  qusgrp  13777  kerf1ghm  13819  cmn32  13849  cmn12  13851  abladdsub  13860  rngass  13910  imasrng  13927  srgass  13942  ringdilem  13983  ringass  13987  imasring  14035  opprrng  14048  opprring  14050  mulgass3  14056  unitgrp  14088  dvrass  14111  dvrdir  14115  subrgunit  14211  issubrg2  14213  aprap  14258  islss3  14351  sralmod  14422  icnpimaex  14893  cnptopresti  14920  upxp  14954  psmettri  15012  isxmet2d  15030  xmettri  15054  metrtri  15059  xmetres2  15061  bldisj  15083  blss2ps  15088  blss2  15089  xmstri2  15152  mstri2  15153  xmstri  15154  mstri  15155  xmstri3  15156  mstri3  15157  msrtri  15158  comet  15181  bdbl  15185  xmetxp  15189  dvconst  15376  dvconstre  15378  dvconstss  15380  sgmmul  15678  findset  16332  pw1ndom3  16383