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  5946  caovlem2d  6198  tfrlemibacc  6472  tfrlemibfn  6474  tfr1onlembacc  6488  tfr1onlembfn  6490  tfrcllembacc  6501  tfrcllembfn  6503  eqsupti  7163  prmuloc2  7754  ltntri  8274  elioc2  10132  elico2  10133  elicc2  10134  fseq1p1m1  10290  elfz0ubfz0  10321  ico0  10481  seq3f1olemp  10737  seq3f1oleml  10738  bcval5  10985  swrdsbslen  11198  ccatswrd  11202  isumss2  11904  tanaddap  12250  dvds2ln  12335  divalglemeunn  12432  divalglemex  12433  divalglemeuneg  12434  qredeq  12618  pcdvdstr  12850  isstructr  13047  prdssgrpd  13448  prdsmndd  13481  imasmnd2  13485  mndissubm  13508  grpsubrcan  13614  grpsubadd  13621  grpsubsub  13622  grpaddsubass  13623  grpsubsub4  13626  grpnnncan2  13630  imasgrp2  13647  mulgnndir  13688  mulgnn0dir  13689  mulgdir  13691  mulgnnass  13694  mulgnn0ass  13695  mulgass  13696  mulgsubdir  13699  issubg2m  13726  eqgval  13760  qusgrp  13769  kerf1ghm  13811  cmn32  13841  cmn12  13843  abladdsub  13852  rngass  13902  imasrng  13919  srgass  13934  ringdilem  13975  ringass  13979  imasring  14027  opprrng  14040  opprring  14042  mulgass3  14048  unitgrp  14080  dvrass  14103  dvrdir  14107  subrgunit  14203  issubrg2  14205  aprap  14250  islss3  14343  sralmod  14414  icnpimaex  14885  cnptopresti  14912  upxp  14946  psmettri  15004  isxmet2d  15022  xmettri  15046  metrtri  15051  xmetres2  15053  bldisj  15075  blss2ps  15080  blss2  15081  xmstri2  15144  mstri2  15145  xmstri  15146  mstri  15147  xmstri3  15148  mstri3  15149  msrtri  15150  comet  15173  bdbl  15177  xmetxp  15181  dvconst  15368  dvconstre  15370  dvconstss  15372  sgmmul  15670  findset  16308