Theorem simpr2 1030

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

Assertion

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

Proof of Theorem simpr2

Step	Hyp	Ref	Expression
1		simp2 1024	. 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:  simplr2  1066  simprr2  1072  simp1r2  1120  simp2r2  1126  simp3r2  1132  3anandis  1383  isopolem  5968  tfrlemibacc  6497  tfrlemibfn  6499  tfr1onlembacc  6513  tfr1onlembfn  6515  tfrcllembacc  6526  tfrcllembfn  6528  prltlu  7712  prdisj  7717  prmuloc2  7792  ltntri  8312  eluzuzle  9769  xlesubadd  10123  elioc2  10176  elico2  10177  elicc2  10178  fseq1p1m1  10334  fz0fzelfz0  10367  seq3f1olemp  10783  bcval5  11031  hashdifpr  11090  hashtpgim  11115  swrdsbslen  11256  ccatswrd  11260  swrdswrdlem  11294  summodclem2  11966  isumss2  11977  tanaddap  12323  dvds2ln  12408  divalglemeunn  12505  divalglemex  12506  divalglemeuneg  12507  isstructr  13120  f1ovscpbl  13418  prdssgrpd  13521  prdsmndd  13554  mndissubm  13581  grpsubrcan  13687  grpsubadd  13694  grpaddsubass  13696  grpsubsub4  13699  grppnpcan2  13700  grpnpncan  13701  mulgnndir  13761  mulgnn0dir  13762  mulgdir  13764  mulgnnass  13767  mulgnn0ass  13768  mulgass  13769  mulgsubdir  13772  issubg2m  13799  eqgval  13833  qusgrp  13842  cmn32  13914  cmn12  13916  abladdsub  13925  ablsubsub23  13935  rngass  13976  srgdilem  14006  srgass  14008  ringdilem  14049  ringass  14053  opprrng  14114  opprring  14116  mulgass3  14122  unitgrp  14154  dvrass  14177  dvrdir  14181  subrgunit  14277  issubrg2  14279  aprap  14324  lsssn0  14408  islss3  14417  sralmod  14488  restopnb  14934  icnpimaex  14964  cnptopresti  14991  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  gausslemma2dlem1a  15816  pw1ndom3  16649