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  5955  caovlem2d  6207  tfrlemibacc  6483  tfrlemibfn  6485  tfr1onlembacc  6499  tfr1onlembfn  6501  tfrcllembacc  6512  tfrcllembfn  6514  eqsupti  7179  prmuloc2  7770  ltntri  8290  elioc2  10149  elico2  10150  elicc2  10151  fseq1p1m1  10307  elfz0ubfz0  10338  ico0  10498  seq3f1olemp  10754  seq3f1oleml  10755  bcval5  11002  swrdsbslen  11219  ccatswrd  11223  isumss2  11925  tanaddap  12271  dvds2ln  12356  divalglemeunn  12453  divalglemex  12454  divalglemeuneg  12455  qredeq  12639  pcdvdstr  12871  isstructr  13068  prdssgrpd  13469  prdsmndd  13502  imasmnd2  13506  mndissubm  13529  grpsubrcan  13635  grpsubadd  13642  grpsubsub  13643  grpaddsubass  13644  grpsubsub4  13647  grpnnncan2  13651  imasgrp2  13668  mulgnndir  13709  mulgnn0dir  13710  mulgdir  13712  mulgnnass  13715  mulgnn0ass  13716  mulgass  13717  mulgsubdir  13720  issubg2m  13747  eqgval  13781  qusgrp  13790  kerf1ghm  13832  cmn32  13862  cmn12  13864  abladdsub  13873  rngass  13923  imasrng  13940  srgass  13955  ringdilem  13996  ringass  14000  imasring  14048  opprrng  14061  opprring  14063  mulgass3  14069  unitgrp  14101  dvrass  14124  dvrdir  14128  subrgunit  14224  issubrg2  14226  aprap  14271  islss3  14364  sralmod  14435  icnpimaex  14906  cnptopresti  14933  upxp  14967  psmettri  15025  isxmet2d  15043  xmettri  15067  metrtri  15072  xmetres2  15074  bldisj  15096  blss2ps  15101  blss2  15102  xmstri2  15165  mstri2  15166  xmstri  15167  mstri  15168  xmstri3  15169  mstri3  15170  msrtri  15171  comet  15194  bdbl  15198  xmetxp  15202  dvconst  15389  dvconstre  15391  dvconstss  15393  sgmmul  15691  findset  16417  pw1ndom3  16467