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 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜓)

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

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 1011

This theorem is referenced by:  simplr1  1070  simprr1  1076  simp1r1  1124  simp2r1  1130  simp3r1  1136  3anandis  1388  isopolem  6022  caovlem2d  6276  suppfnss  6491  tfrlemibacc  6591  tfrlemibfn  6593  tfr1onlembacc  6607  tfr1onlembfn  6609  tfrcllembacc  6620  tfrcllembfn  6622  eqsupti  7330  prmuloc2  7928  ltntri  8448  elioc2  10321  elico2  10322  elicc2  10323  fseq1p1m1  10484  elfz0ubfz0  10515  ico0  10679  seq3f1olemp  10935  seq3f1oleml  10936  bcval5  11184  hashtpgim  11280  swrdsbslen  11421  ccatswrd  11425  isumss2  12143  tanaddap  12489  dvds2ln  12574  divalglemeunn  12671  divalglemex  12672  divalglemeuneg  12673  qredeq  12857  pcdvdstr  13089  isstructr  13350  imasmnd2  13742  mndissubm  13765  grpsubrcan  13869  grpsubadd  13876  grpsubsub  13877  grpaddsubass  13878  grpsubsub4  13881  grpnnncan2  13885  imasgrp2  13896  mulgnndir  13937  mulgnn0dir  13938  mulgdir  13940  mulgnnass  13943  mulgnn0ass  13944  mulgass  13945  mulgsubdir  13948  issubg2m  13975  eqgval  14009  qusgrp  14018  kerf1ghm  14060  cmn32  14090  cmn12  14092  abladdsub  14102  prdssgrpd  14174  prdsmndd  14177  rngass  14221  imasrng  14238  srgass  14258  ringdilem  14299  ringass  14303  imasring  14352  opprrng  14365  opprring  14367  mulgass3  14374  unitgrp  14406  dvrass  14429  dvrdir  14433  subrgunit  14530  issubrg2  14532  aprap  14581  islss3  14699  sralmod  14770  icnpimaex  15295  cnptopresti  15322  upxp  15356  psmettri  15414  isxmet2d  15432  xmettri  15456  metrtri  15461  xmetres2  15463  bldisj  15485  blss2ps  15490  blss2  15491  xmstri2  15554  mstri2  15555  xmstri  15556  mstri  15557  xmstri3  15558  mstri3  15559  msrtri  15560  comet  15583  bdbl  15587  xmetxp  15591  dvconst  15778  dvconstre  15780  dvconstss  15782  sgmmul  16093  findset  16954  pw1ndom3  17003