Theorem simpr2 1009

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

Assertion

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

Proof of Theorem simpr2

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

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

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 985

This theorem is referenced by:  simplr2  1045  simprr2  1051  simp1r2  1099  simp2r2  1105  simp3r2  1111  3anandis  1362  isopolem  5919  tfrlemibacc  6442  tfrlemibfn  6444  tfr1onlembacc  6458  tfr1onlembfn  6460  tfrcllembacc  6471  tfrcllembfn  6473  prltlu  7642  prdisj  7647  prmuloc2  7722  ltntri  8242  eluzuzle  9698  xlesubadd  10047  elioc2  10100  elico2  10101  elicc2  10102  fseq1p1m1  10258  fz0fzelfz0  10291  seq3f1olemp  10704  bcval5  10952  hashdifpr  11009  swrdsbslen  11164  ccatswrd  11168  swrdswrdlem  11202  summodclem2  11859  isumss2  11870  tanaddap  12216  dvds2ln  12301  divalglemeunn  12398  divalglemex  12399  divalglemeuneg  12400  isstructr  13013  f1ovscpbl  13311  prdssgrpd  13414  prdsmndd  13447  mndissubm  13474  grpsubrcan  13580  grpsubadd  13587  grpaddsubass  13589  grpsubsub4  13592  grppnpcan2  13593  grpnpncan  13594  mulgnndir  13654  mulgnn0dir  13655  mulgdir  13657  mulgnnass  13660  mulgnn0ass  13661  mulgass  13662  mulgsubdir  13665  issubg2m  13692  eqgval  13726  qusgrp  13735  cmn32  13807  cmn12  13809  abladdsub  13818  ablsubsub23  13828  rngass  13868  srgdilem  13898  srgass  13900  ringdilem  13941  ringass  13945  opprrng  14006  opprring  14008  mulgass3  14014  unitgrp  14045  dvrass  14068  dvrdir  14072  subrgunit  14168  issubrg2  14170  aprap  14215  lsssn0  14299  islss3  14308  sralmod  14379  restopnb  14820  icnpimaex  14850  cnptopresti  14877  psmettri  14969  isxmet2d  14987  xmettri  15011  metrtri  15016  xmetres2  15018  bldisj  15040  blss2ps  15045  blss2  15046  xmstri2  15109  mstri2  15110  xmstri  15111  mstri  15112  xmstri3  15113  mstri3  15114  msrtri  15115  comet  15138  bdbl  15142  xmetxp  15146  dvconst  15333  dvconstre  15335  dvconstss  15337  sgmmul  15635  gausslemma2dlem1a  15702