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  5963  tfrlemibacc  6492  tfrlemibfn  6494  tfr1onlembacc  6508  tfr1onlembfn  6510  tfrcllembacc  6521  tfrcllembfn  6523  prltlu  7707  prdisj  7712  prmuloc2  7787  ltntri  8307  eluzuzle  9764  xlesubadd  10118  elioc2  10171  elico2  10172  elicc2  10173  fseq1p1m1  10329  fz0fzelfz0  10362  seq3f1olemp  10778  bcval5  11026  hashdifpr  11085  swrdsbslen  11248  ccatswrd  11252  swrdswrdlem  11286  summodclem2  11945  isumss2  11956  tanaddap  12302  dvds2ln  12387  divalglemeunn  12484  divalglemex  12485  divalglemeuneg  12486  isstructr  13099  f1ovscpbl  13397  prdssgrpd  13500  prdsmndd  13533  mndissubm  13560  grpsubrcan  13666  grpsubadd  13673  grpaddsubass  13675  grpsubsub4  13678  grppnpcan2  13679  grpnpncan  13680  mulgnndir  13740  mulgnn0dir  13741  mulgdir  13743  mulgnnass  13746  mulgnn0ass  13747  mulgass  13748  mulgsubdir  13751  issubg2m  13778  eqgval  13812  qusgrp  13821  cmn32  13893  cmn12  13895  abladdsub  13904  ablsubsub23  13914  rngass  13955  srgdilem  13985  srgass  13987  ringdilem  14028  ringass  14032  opprrng  14093  opprring  14095  mulgass3  14101  unitgrp  14133  dvrass  14156  dvrdir  14160  subrgunit  14256  issubrg2  14258  aprap  14303  lsssn0  14387  islss3  14396  sralmod  14467  restopnb  14908  icnpimaex  14938  cnptopresti  14965  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  gausslemma2dlem1a  15790  pw1ndom3  16610