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  5968  caovlem2d  6220  tfrlemibacc  6497  tfrlemibfn  6499  tfr1onlembacc  6513  tfr1onlembfn  6515  tfrcllembacc  6526  tfrcllembfn  6528  eqsupti  7200  prmuloc2  7792  ltntri  8312  elioc2  10176  elico2  10177  elicc2  10178  fseq1p1m1  10334  elfz0ubfz0  10365  ico0  10527  seq3f1olemp  10783  seq3f1oleml  10784  bcval5  11031  hashtpgim  11115  swrdsbslen  11256  ccatswrd  11260  isumss2  11977  tanaddap  12323  dvds2ln  12408  divalglemeunn  12505  divalglemex  12506  divalglemeuneg  12507  qredeq  12691  pcdvdstr  12923  isstructr  13120  prdssgrpd  13521  prdsmndd  13554  imasmnd2  13558  mndissubm  13581  grpsubrcan  13687  grpsubadd  13694  grpsubsub  13695  grpaddsubass  13696  grpsubsub4  13699  grpnnncan2  13703  imasgrp2  13720  mulgnndir  13761  mulgnn0dir  13762  mulgdir  13764  mulgnnass  13767  mulgnn0ass  13768  mulgass  13769  mulgsubdir  13772  issubg2m  13799  eqgval  13833  qusgrp  13842  kerf1ghm  13884  cmn32  13914  cmn12  13916  abladdsub  13925  rngass  13976  imasrng  13993  srgass  14008  ringdilem  14049  ringass  14053  imasring  14101  opprrng  14114  opprring  14116  mulgass3  14122  unitgrp  14154  dvrass  14177  dvrdir  14181  subrgunit  14277  issubrg2  14279  aprap  14324  islss3  14417  sralmod  14488  icnpimaex  14964  cnptopresti  14991  upxp  15025  psmettri  15083  isxmet2d  15101  xmettri  15125  metrtri  15130  xmetres2  15132  bldisj  15154  blss2ps  15159  blss2  15160  xmstri2  15223  mstri2  15224  xmstri  15225  mstri  15226  xmstri3  15227  mstri3  15228  msrtri  15229  comet  15252  bdbl  15256  xmetxp  15260  dvconst  15447  dvconstre  15449  dvconstss  15451  sgmmul  15749  findset  16600  pw1ndom3  16649