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  5958  caovlem2d  6210  tfrlemibacc  6487  tfrlemibfn  6489  tfr1onlembacc  6503  tfr1onlembfn  6505  tfrcllembacc  6516  tfrcllembfn  6518  eqsupti  7189  prmuloc2  7780  ltntri  8300  elioc2  10164  elico2  10165  elicc2  10166  fseq1p1m1  10322  elfz0ubfz0  10353  ico0  10514  seq3f1olemp  10770  seq3f1oleml  10771  bcval5  11018  swrdsbslen  11240  ccatswrd  11244  isumss2  11947  tanaddap  12293  dvds2ln  12378  divalglemeunn  12475  divalglemex  12476  divalglemeuneg  12477  qredeq  12661  pcdvdstr  12893  isstructr  13090  prdssgrpd  13491  prdsmndd  13524  imasmnd2  13528  mndissubm  13551  grpsubrcan  13657  grpsubadd  13664  grpsubsub  13665  grpaddsubass  13666  grpsubsub4  13669  grpnnncan2  13673  imasgrp2  13690  mulgnndir  13731  mulgnn0dir  13732  mulgdir  13734  mulgnnass  13737  mulgnn0ass  13738  mulgass  13739  mulgsubdir  13742  issubg2m  13769  eqgval  13803  qusgrp  13812  kerf1ghm  13854  cmn32  13884  cmn12  13886  abladdsub  13895  rngass  13945  imasrng  13962  srgass  13977  ringdilem  14018  ringass  14022  imasring  14070  opprrng  14083  opprring  14085  mulgass3  14091  unitgrp  14123  dvrass  14146  dvrdir  14150  subrgunit  14246  issubrg2  14248  aprap  14293  islss3  14386  sralmod  14457  icnpimaex  14928  cnptopresti  14955  upxp  14989  psmettri  15047  isxmet2d  15065  xmettri  15089  metrtri  15094  xmetres2  15096  bldisj  15118  blss2ps  15123  blss2  15124  xmstri2  15187  mstri2  15188  xmstri  15189  mstri  15190  xmstri3  15191  mstri3  15192  msrtri  15193  comet  15216  bdbl  15220  xmetxp  15224  dvconst  15411  dvconstre  15413  dvconstss  15415  sgmmul  15713  findset  16490  pw1ndom3  16539