Theorem simpr1 1008

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

Assertion

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

Proof of Theorem simpr1

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

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

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 985

This theorem is referenced by:  simplr1  1044  simprr1  1050  simp1r1  1098  simp2r1  1104  simp3r1  1110  3anandis  1362  isopolem  5919  caovlem2d  6169  tfrlemibacc  6442  tfrlemibfn  6444  tfr1onlembacc  6458  tfr1onlembfn  6460  tfrcllembacc  6471  tfrcllembfn  6473  eqsupti  7131  prmuloc2  7722  ltntri  8242  elioc2  10100  elico2  10101  elicc2  10102  fseq1p1m1  10258  elfz0ubfz0  10289  ico0  10448  seq3f1olemp  10704  seq3f1oleml  10705  bcval5  10952  swrdsbslen  11164  ccatswrd  11168  isumss2  11870  tanaddap  12216  dvds2ln  12301  divalglemeunn  12398  divalglemex  12399  divalglemeuneg  12400  qredeq  12584  pcdvdstr  12816  isstructr  13013  prdssgrpd  13414  prdsmndd  13447  imasmnd2  13451  mndissubm  13474  grpsubrcan  13580  grpsubadd  13587  grpsubsub  13588  grpaddsubass  13589  grpsubsub4  13592  grpnnncan2  13596  imasgrp2  13613  mulgnndir  13654  mulgnn0dir  13655  mulgdir  13657  mulgnnass  13660  mulgnn0ass  13661  mulgass  13662  mulgsubdir  13665  issubg2m  13692  eqgval  13726  qusgrp  13735  kerf1ghm  13777  cmn32  13807  cmn12  13809  abladdsub  13818  rngass  13868  imasrng  13885  srgass  13900  ringdilem  13941  ringass  13945  imasring  13993  opprrng  14006  opprring  14008  mulgass3  14014  unitgrp  14045  dvrass  14068  dvrdir  14072  subrgunit  14168  issubrg2  14170  aprap  14215  islss3  14308  sralmod  14379  icnpimaex  14850  cnptopresti  14877  upxp  14911  psmettri  14969  isxmet2d  14987  xmettri  15011  metrtri  15016  xmetres2  15018  bldisj  15040  blss2ps  15045  blss2  15046  xmstri2  15109  mstri2  15110  xmstri  15111  mstri  15112  xmstri3  15113  mstri3  15114  msrtri  15115  comet  15138  bdbl  15142  xmetxp  15146  dvconst  15333  dvconstre  15335  dvconstss  15337  sgmmul  15635  findset  16218