Theorem simpr1 1029

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

Assertion

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

Proof of Theorem simpr1

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

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

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 1006

This theorem is referenced by:  simplr1  1065  simprr1  1071  simp1r1  1119  simp2r1  1125  simp3r1  1131  3anandis  1383  isopolem  5963  caovlem2d  6215  tfrlemibacc  6492  tfrlemibfn  6494  tfr1onlembacc  6508  tfr1onlembfn  6510  tfrcllembacc  6521  tfrcllembfn  6523  eqsupti  7195  prmuloc2  7787  ltntri  8307  elioc2  10171  elico2  10172  elicc2  10173  fseq1p1m1  10329  elfz0ubfz0  10360  ico0  10522  seq3f1olemp  10778  seq3f1oleml  10779  bcval5  11026  swrdsbslen  11248  ccatswrd  11252  isumss2  11956  tanaddap  12302  dvds2ln  12387  divalglemeunn  12484  divalglemex  12485  divalglemeuneg  12486  qredeq  12670  pcdvdstr  12902  isstructr  13099  prdssgrpd  13500  prdsmndd  13533  imasmnd2  13537  mndissubm  13560  grpsubrcan  13666  grpsubadd  13673  grpsubsub  13674  grpaddsubass  13675  grpsubsub4  13678  grpnnncan2  13682  imasgrp2  13699  mulgnndir  13740  mulgnn0dir  13741  mulgdir  13743  mulgnnass  13746  mulgnn0ass  13747  mulgass  13748  mulgsubdir  13751  issubg2m  13778  eqgval  13812  qusgrp  13821  kerf1ghm  13863  cmn32  13893  cmn12  13895  abladdsub  13904  rngass  13955  imasrng  13972  srgass  13987  ringdilem  14028  ringass  14032  imasring  14080  opprrng  14093  opprring  14095  mulgass3  14101  unitgrp  14133  dvrass  14156  dvrdir  14160  subrgunit  14256  issubrg2  14258  aprap  14303  islss3  14396  sralmod  14467  icnpimaex  14938  cnptopresti  14965  upxp  14999  psmettri  15057  isxmet2d  15075  xmettri  15099  metrtri  15104  xmetres2  15106  bldisj  15128  blss2ps  15133  blss2  15134  xmstri2  15197  mstri2  15198  xmstri  15199  mstri  15200  xmstri3  15201  mstri3  15202  msrtri  15203  comet  15226  bdbl  15230  xmetxp  15234  dvconst  15421  dvconstre  15423  dvconstss  15425  sgmmul  15723  findset  16561  pw1ndom3  16610