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  6031  caovlem2d  6285  suppfnss  6501  tfrlemibacc  6601  tfrlemibfn  6603  tfr1onlembacc  6617  tfr1onlembfn  6619  tfrcllembacc  6630  tfrcllembfn  6632  eqsupti  7343  prmuloc2  7941  ltntri  8462  elioc2  10356  elico2  10357  elicc2  10358  fseq1p1m1  10519  elfz0ubfz0  10550  ico0  10714  seq3f1olemp  10974  seq3f1oleml  10975  bcval5  11224  hashtpgim  11320  swrdsbslen  11461  ccatswrd  11465  isumss2  12186  tanaddap  12532  dvds2ln  12617  divalglemeunn  12714  divalglemex  12715  divalglemeuneg  12716  qredeq  12900  pcdvdstr  13136  isstructr  13426  imasmnd2  13819  mndissubm  13842  grpsubrcan  13946  grpsubadd  13953  grpsubsub  13954  grpaddsubass  13955  grpsubsub4  13958  grpnnncan2  13962  imasgrp2  13973  mulgnndir  14014  mulgnn0dir  14015  mulgdir  14017  mulgnnass  14020  mulgnn0ass  14021  mulgass  14022  mulgsubdir  14025  issubg2m  14052  eqgval  14086  qusgrp  14095  kerf1ghm  14137  cmn32  14198  cmn12  14200  abladdsub  14210  prdssgrpd  14299  prdsmndd  14302  rngass  14346  imasrng  14363  srgass  14383  ringdilem  14424  ringass  14428  imasring  14479  opprrng  14492  opprring  14494  mulgass3  14501  unitgrp  14533  dvrass  14556  dvrdir  14560  subrgunit  14657  issubrg2  14659  aprap  14708  islss3  14826  sralmod  14897  psrringfi  15209  icnpimaex  15449  cnptopresti  15476  upxp  15510  psmettri  15568  isxmet2d  15586  xmettri  15610  metrtri  15615  xmetres2  15617  bldisj  15639  blss2ps  15644  blss2  15645  xmstri2  15708  mstri2  15709  xmstri  15710  mstri  15711  xmstri3  15712  mstri3  15713  msrtri  15714  comet  15737  bdbl  15741  xmetxp  15745  dvconst  15932  dvconstre  15934  dvconstss  15936  sgmmul  16302  findset  17188  pw1ndom3  17237