Theorem simpr2 1028

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

Assertion

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

Proof of Theorem simpr2

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

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

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 1004

This theorem is referenced by:  simplr2  1064  simprr2  1070  simp1r2  1118  simp2r2  1124  simp3r2  1130  3anandis  1381  isopolem  5958  tfrlemibacc  6487  tfrlemibfn  6489  tfr1onlembacc  6503  tfr1onlembfn  6505  tfrcllembacc  6516  tfrcllembfn  6518  prltlu  7700  prdisj  7705  prmuloc2  7780  ltntri  8300  eluzuzle  9757  xlesubadd  10111  elioc2  10164  elico2  10165  elicc2  10166  fseq1p1m1  10322  fz0fzelfz0  10355  seq3f1olemp  10770  bcval5  11018  hashdifpr  11077  swrdsbslen  11240  ccatswrd  11244  swrdswrdlem  11278  summodclem2  11936  isumss2  11947  tanaddap  12293  dvds2ln  12378  divalglemeunn  12475  divalglemex  12476  divalglemeuneg  12477  isstructr  13090  f1ovscpbl  13388  prdssgrpd  13491  prdsmndd  13524  mndissubm  13551  grpsubrcan  13657  grpsubadd  13664  grpaddsubass  13666  grpsubsub4  13669  grppnpcan2  13670  grpnpncan  13671  mulgnndir  13731  mulgnn0dir  13732  mulgdir  13734  mulgnnass  13737  mulgnn0ass  13738  mulgass  13739  mulgsubdir  13742  issubg2m  13769  eqgval  13803  qusgrp  13812  cmn32  13884  cmn12  13886  abladdsub  13895  ablsubsub23  13905  rngass  13945  srgdilem  13975  srgass  13977  ringdilem  14018  ringass  14022  opprrng  14083  opprring  14085  mulgass3  14091  unitgrp  14123  dvrass  14146  dvrdir  14150  subrgunit  14246  issubrg2  14248  aprap  14293  lsssn0  14377  islss3  14386  sralmod  14457  restopnb  14898  icnpimaex  14928  cnptopresti  14955  psmettri  15047  isxmet2d  15065  xmettri  15089  metrtri  15094  xmetres2  15096  bldisj  15118  blss2ps  15123  blss2  15124  xmstri2  15187  mstri2  15188  xmstri  15189  mstri  15190  xmstri3  15191  mstri3  15192  msrtri  15193  comet  15216  bdbl  15220  xmetxp  15224  dvconst  15411  dvconstre  15413  dvconstss  15415  sgmmul  15713  gausslemma2dlem1a  15780  pw1ndom3  16539