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  6001  caovlem2d  6255  suppfnss  6470  tfrlemibacc  6570  tfrlemibfn  6572  tfr1onlembacc  6586  tfr1onlembfn  6588  tfrcllembacc  6599  tfrcllembfn  6601  eqsupti  7300  prmuloc2  7898  ltntri  8418  elioc2  10291  elico2  10292  elicc2  10293  fseq1p1m1  10453  elfz0ubfz0  10484  ico0  10648  seq3f1olemp  10904  seq3f1oleml  10905  bcval5  11153  hashtpgim  11245  swrdsbslen  11386  ccatswrd  11390  isumss2  12107  tanaddap  12453  dvds2ln  12538  divalglemeunn  12635  divalglemex  12636  divalglemeuneg  12637  qredeq  12821  pcdvdstr  13053  isstructr  13314  imasmnd2  13710  mndissubm  13733  grpsubrcan  13839  grpsubadd  13846  grpsubsub  13847  grpaddsubass  13848  grpsubsub4  13851  grpnnncan2  13855  imasgrp2  13866  mulgnndir  13907  mulgnn0dir  13908  mulgdir  13910  mulgnnass  13913  mulgnn0ass  13914  mulgass  13915  mulgsubdir  13918  issubg2m  13945  eqgval  13979  qusgrp  13988  kerf1ghm  14030  cmn32  14060  cmn12  14062  abladdsub  14071  prdssgrpd  14136  prdsmndd  14139  rngass  14181  imasrng  14198  srgass  14217  ringdilem  14258  ringass  14262  imasring  14310  opprrng  14323  opprring  14325  mulgass3  14332  unitgrp  14364  dvrass  14387  dvrdir  14391  subrgunit  14488  issubrg2  14490  aprap  14539  islss3  14656  sralmod  14727  icnpimaex  15205  cnptopresti  15232  upxp  15266  psmettri  15324  isxmet2d  15342  xmettri  15366  metrtri  15371  xmetres2  15373  bldisj  15395  blss2ps  15400  blss2  15401  xmstri2  15464  mstri2  15465  xmstri  15466  mstri  15467  xmstri3  15468  mstri3  15469  msrtri  15470  comet  15493  bdbl  15497  xmetxp  15501  dvconst  15688  dvconstre  15690  dvconstss  15692  sgmmul  15993  findset  16854  pw1ndom3  16903