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 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜒)

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

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 1011

This theorem is referenced by:  simplr2  1071  simprr2  1077  simp1r2  1125  simp2r2  1131  simp3r2  1137  3anandis  1388  isopolem  6022  tfrlemibacc  6591  tfrlemibfn  6593  tfr1onlembacc  6607  tfr1onlembfn  6609  tfrcllembacc  6620  tfrcllembfn  6622  prltlu  7848  prdisj  7853  prmuloc2  7928  ltntri  8448  eluzuzle  9913  xlesubadd  10268  elioc2  10321  elico2  10322  elicc2  10323  fseq1p1m1  10484  fz0fzelfz0  10517  seq3f1olemp  10935  bcval5  11184  hashdifpr  11244  hashtpgim  11280  swrdsbslen  11421  ccatswrd  11425  swrdswrdlem  11459  summodclem2  12132  isumss2  12143  tanaddap  12489  dvds2ln  12574  divalglemeunn  12671  divalglemex  12672  divalglemeuneg  12673  isstructr  13350  f1ovscpbl  13616  mndissubm  13765  grpsubrcan  13869  grpsubadd  13876  grpaddsubass  13878  grpsubsub4  13881  grppnpcan2  13882  grpnpncan  13883  mulgnndir  13937  mulgnn0dir  13938  mulgdir  13940  mulgnnass  13943  mulgnn0ass  13944  mulgass  13945  mulgsubdir  13948  issubg2m  13975  eqgval  14009  qusgrp  14018  cmn32  14090  cmn12  14092  abladdsub  14102  ablsubsub23  14112  prdssgrpd  14174  prdsmndd  14177  rngass  14221  srgdilem  14256  srgass  14258  ringdilem  14299  ringass  14303  opprrng  14365  opprring  14367  mulgass3  14374  unitgrp  14406  dvrass  14429  dvrdir  14433  subrgunit  14530  issubrg2  14532  aprap  14581  lsssn0  14690  islss3  14699  sralmod  14770  restopnb  15265  icnpimaex  15295  cnptopresti  15322  psmettri  15414  isxmet2d  15432  xmettri  15456  metrtri  15461  xmetres2  15463  bldisj  15485  blss2ps  15490  blss2  15491  xmstri2  15554  mstri2  15555  xmstri  15556  mstri  15557  xmstri3  15558  mstri3  15559  msrtri  15560  comet  15583  bdbl  15587  xmetxp  15591  dvconst  15778  dvconstre  15780  dvconstss  15782  sgmmul  16093  gausslemma2dlem1a  16160  pw1ndom3  17003