Theorem simpr2 1031

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

Assertion

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

Proof of Theorem simpr2

Step	Hyp	Ref	Expression
1		simp2 1025	. 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:  simplr2  1067  simprr2  1073  simp1r2  1121  simp2r2  1127  simp3r2  1133  3anandis  1384  isopolem  5994  tfrlemibacc  6556  tfrlemibfn  6558  tfr1onlembacc  6572  tfr1onlembfn  6574  tfrcllembacc  6585  tfrcllembfn  6587  prltlu  7798  prdisj  7803  prmuloc2  7878  ltntri  8397  eluzuzle  9858  xlesubadd  10212  elioc2  10265  elico2  10266  elicc2  10267  fseq1p1m1  10424  fz0fzelfz0  10457  seq3f1olemp  10873  bcval5  11121  hashdifpr  11180  hashtpgim  11210  swrdsbslen  11351  ccatswrd  11355  swrdswrdlem  11389  summodclem2  12061  isumss2  12072  tanaddap  12418  dvds2ln  12503  divalglemeunn  12600  divalglemex  12601  divalglemeuneg  12602  isstructr  13216  f1ovscpbl  13514  prdssgrpd  13617  prdsmndd  13650  mndissubm  13677  grpsubrcan  13783  grpsubadd  13790  grpaddsubass  13792  grpsubsub4  13795  grppnpcan2  13796  grpnpncan  13797  mulgnndir  13857  mulgnn0dir  13858  mulgdir  13860  mulgnnass  13863  mulgnn0ass  13864  mulgass  13865  mulgsubdir  13868  issubg2m  13895  eqgval  13929  qusgrp  13938  cmn32  14010  cmn12  14012  abladdsub  14021  ablsubsub23  14031  rngass  14072  srgdilem  14102  srgass  14104  ringdilem  14145  ringass  14149  opprrng  14210  opprring  14212  mulgass3  14218  unitgrp  14250  dvrass  14273  dvrdir  14277  subrgunit  14373  issubrg2  14375  aprap  14421  lsssn0  14505  islss3  14514  sralmod  14585  restopnb  15033  icnpimaex  15063  cnptopresti  15090  psmettri  15182  isxmet2d  15200  xmettri  15224  metrtri  15229  xmetres2  15231  bldisj  15253  blss2ps  15258  blss2  15259  xmstri2  15322  mstri2  15323  xmstri  15324  mstri  15325  xmstri3  15326  mstri3  15327  msrtri  15328  comet  15351  bdbl  15355  xmetxp  15359  dvconst  15546  dvconstre  15548  dvconstss  15550  sgmmul  15851  gausslemma2dlem1a  15918  pw1ndom3  16751