Theorem simpr2 1035

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

Assertion

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

Proof of Theorem simpr2

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  simplr2  1071  simprr2  1077  simp1r2  1125  simp2r2  1131  simp3r2  1137  3anandis  1388  isopolem  6028  tfrlemibacc  6597  tfrlemibfn  6599  tfr1onlembacc  6613  tfr1onlembfn  6615  tfrcllembacc  6626  tfrcllembfn  6628  prltlu  7855  prdisj  7860  prmuloc2  7935  ltntri  8456  eluzuzle  9940  xlesubadd  10296  elioc2  10349  elico2  10350  elicc2  10351  fseq1p1m1  10512  fz0fzelfz0  10545  seq3f1olemp  10967  bcval5  11217  hashdifpr  11277  hashtpgim  11313  swrdsbslen  11454  ccatswrd  11458  swrdswrdlem  11492  summodclem2  12168  isumss2  12179  tanaddap  12525  dvds2ln  12610  divalglemeunn  12707  divalglemex  12708  divalglemeuneg  12709  isstructr  13419  f1ovscpbl  13686  mndissubm  13835  grpsubrcan  13939  grpsubadd  13946  grpaddsubass  13948  grpsubsub4  13951  grppnpcan2  13952  grpnpncan  13953  mulgnndir  14007  mulgnn0dir  14008  mulgdir  14010  mulgnnass  14013  mulgnn0ass  14014  mulgass  14015  mulgsubdir  14018  issubg2m  14045  eqgval  14079  qusgrp  14088  cmn32  14191  cmn12  14193  abladdsub  14203  ablsubsub23  14213  prdssgrpd  14282  prdsmndd  14285  rngass  14329  srgdilem  14364  srgass  14366  ringdilem  14407  ringass  14411  opprrng  14473  opprring  14475  mulgass3  14482  unitgrp  14514  dvrass  14537  dvrdir  14541  subrgunit  14638  issubrg2  14640  aprap  14689  lsssn0  14798  islss3  14807  sralmod  14878  restopnb  15381  icnpimaex  15411  cnptopresti  15438  psmettri  15530  isxmet2d  15548  xmettri  15572  metrtri  15577  xmetres2  15579  bldisj  15601  blss2ps  15606  blss2  15607  xmstri2  15670  mstri2  15671  xmstri  15672  mstri  15673  xmstri3  15674  mstri3  15675  msrtri  15676  comet  15699  bdbl  15703  xmetxp  15707  dvconst  15894  dvconstre  15896  dvconstss  15898  sgmmul  16264  gausslemma2dlem1a  16356  pw1ndom3  17199