Theorem simpr3 1029

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

Assertion

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

Proof of Theorem simpr3

Step	Hyp	Ref	Expression
1		simp3 1023	. 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:  simplr3  1065  simprr3  1071  simp1r3  1119  simp2r3  1125  simp3r3  1131  3anandis  1381  isopolem  5952  tfrlemibacc  6478  tfrlemibxssdm  6479  tfrlemibfn  6480  tfr1onlembacc  6494  tfr1onlembxssdm  6495  tfr1onlembfn  6496  tfrcllembacc  6507  tfrcllembxssdm  6508  tfrcllembfn  6509  elfir  7148  prloc  7686  prmuloc2  7762  ltntri  8282  eluzuzle  9738  xlesubadd  10087  elioc2  10140  elico2  10141  elicc2  10142  fseq1p1m1  10298  seq3f1olemp  10745  seq3f1oleml  10746  bcval5  10993  hashdifpr  11050  ccatswrd  11210  pfxccat3a  11278  isumss2  11912  tanaddap  12258  dvds2ln  12343  divalglemeunn  12440  divalglemex  12441  divalglemeuneg  12442  f1ovscpbl  13353  prdssgrpd  13456  prdsmndd  13489  imasmnd2  13493  imasmnd  13494  grpsubadd  13629  grpaddsubass  13631  grpsubsub4  13634  grppnpcan2  13635  grpnpncan  13636  grpnnncan2  13638  imasgrp2  13655  imasgrp  13656  mulgnndir  13696  mulgnn0dir  13697  mulgnnass  13702  mulgnn0ass  13703  mulgass  13704  issubg2m  13734  qusgrp  13777  kerf1ghm  13819  cmn32  13849  cmn12  13851  abladdsub  13860  ablsubsub23  13870  rngass  13910  imasrng  13927  srgdilem  13940  srgass  13942  ringdilem  13983  ringass  13987  ringrng  14007  imasring  14035  opprrng  14048  opprring  14050  mulgass3  14056  unitgrp  14088  dvrass  14111  dvrdir  14115  subrgunit  14211  issubrg2  14213  aprap  14258  lss1  14334  lsssn0  14342  islss3  14351  sralmod  14422  restopnb  14863  icnpimaex  14893  cnptopresti  14920  psmettri  15012  isxmet2d  15030  xmettri  15054  metrtri  15059  xmetres2  15061  bldisj  15083  blss2ps  15088  blss2  15089  xmstri2  15152  mstri2  15153  xmstri  15154  mstri  15155  xmstri3  15156  mstri3  15157  msrtri  15158  comet  15181  bdbl  15185  xmetxp  15189  dvconst  15376  dvconstre  15378  dvconstss  15380  sgmmul  15678  pw1ndom3  16383