Theorem simpr1 1030

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

Assertion

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

Proof of Theorem simpr1

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

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

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 1007

This theorem is referenced by:  simplr1  1066  simprr1  1072  simp1r1  1120  simp2r1  1126  simp3r1  1132  3anandis  1384  isopolem  5997  caovlem2d  6249  suppfnss  6459  tfrlemibacc  6559  tfrlemibfn  6561  tfr1onlembacc  6575  tfr1onlembfn  6577  tfrcllembacc  6588  tfrcllembfn  6590  eqsupti  7289  prmuloc2  7887  ltntri  8406  elioc2  10275  elico2  10276  elicc2  10277  fseq1p1m1  10435  elfz0ubfz0  10466  ico0  10628  seq3f1olemp  10884  seq3f1oleml  10885  bcval5  11133  hashtpgim  11225  swrdsbslen  11366  ccatswrd  11370  isumss2  12087  tanaddap  12433  dvds2ln  12518  divalglemeunn  12615  divalglemex  12616  divalglemeuneg  12617  qredeq  12801  pcdvdstr  13033  isstructr  13248  prdssgrpd  13649  prdsmndd  13682  imasmnd2  13686  mndissubm  13709  grpsubrcan  13815  grpsubadd  13822  grpsubsub  13823  grpaddsubass  13824  grpsubsub4  13827  grpnnncan2  13831  imasgrp2  13848  mulgnndir  13889  mulgnn0dir  13890  mulgdir  13892  mulgnnass  13895  mulgnn0ass  13896  mulgass  13897  mulgsubdir  13900  issubg2m  13927  eqgval  13961  qusgrp  13970  kerf1ghm  14012  cmn32  14042  cmn12  14044  abladdsub  14053  rngass  14104  imasrng  14121  srgass  14136  ringdilem  14177  ringass  14181  imasring  14229  opprrng  14242  opprring  14244  mulgass3  14251  unitgrp  14283  dvrass  14306  dvrdir  14310  subrgunit  14407  issubrg2  14409  aprap  14458  islss3  14576  sralmod  14647  icnpimaex  15125  cnptopresti  15152  upxp  15186  psmettri  15244  isxmet2d  15262  xmettri  15286  metrtri  15291  xmetres2  15293  bldisj  15315  blss2ps  15320  blss2  15321  xmstri2  15384  mstri2  15385  xmstri  15386  mstri  15387  xmstri3  15388  mstri3  15389  msrtri  15390  comet  15413  bdbl  15417  xmetxp  15421  dvconst  15608  dvconstre  15610  dvconstss  15612  sgmmul  15913  findset  16764  pw1ndom3  16813