Theorem simpr3 1036

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

Assertion

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

Proof of Theorem simpr3

Step	Hyp	Ref	Expression
1		simp3 1030	. 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:  simplr3  1072  simprr3  1078  simp1r3  1126  simp2r3  1132  simp3r3  1138  3anandis  1388  isopolem  6028  suppfnss  6497  tfrlemibacc  6597  tfrlemibxssdm  6598  tfrlemibfn  6599  tfr1onlembacc  6613  tfr1onlembxssdm  6614  tfr1onlembfn  6615  tfrcllembacc  6626  tfrcllembxssdm  6627  tfrcllembfn  6628  elfir  7307  prloc  7858  prmuloc2  7934  ltntri  8454  eluzuzle  9932  xlesubadd  10287  elioc2  10340  elico2  10341  elicc2  10342  fseq1p1m1  10503  seq3f1olemp  10954  seq3f1oleml  10955  bcval5  11203  hashdifpr  11263  hashtpgim  11299  ccatswrd  11444  pfxccat3a  11512  isumss2  12162  tanaddap  12508  dvds2ln  12593  divalglemeunn  12690  divalglemex  12691  divalglemeuneg  12692  f1ovscpbl  13635  imasmnd2  13761  imasmnd  13762  grpsubadd  13895  grpaddsubass  13897  grpsubsub4  13900  grppnpcan2  13901  grpnpncan  13902  grpnnncan2  13904  imasgrp2  13915  imasgrp  13916  mulgnndir  13956  mulgnn0dir  13957  mulgnnass  13962  mulgnn0ass  13963  mulgass  13964  issubg2m  13994  qusgrp  14037  kerf1ghm  14079  cmn32  14109  cmn12  14111  abladdsub  14121  ablsubsub23  14131  prdssgrpd  14193  prdsmndd  14196  rngass  14240  imasrng  14257  srgdilem  14275  srgass  14277  ringdilem  14318  ringass  14322  ringrng  14343  imasring  14371  opprrng  14384  opprring  14386  mulgass3  14393  unitgrp  14425  dvrass  14448  dvrdir  14452  subrgunit  14549  issubrg2  14551  aprap  14600  lss1  14701  lsssn0  14709  islss3  14718  sralmod  14789  restopnb  15284  icnpimaex  15314  cnptopresti  15341  psmettri  15433  isxmet2d  15451  xmettri  15475  metrtri  15480  xmetres2  15482  bldisj  15504  blss2ps  15509  blss2  15510  xmstri2  15573  mstri2  15574  xmstri  15575  mstri  15576  xmstri3  15577  mstri3  15578  msrtri  15579  comet  15602  bdbl  15606  xmetxp  15610  dvconst  15797  dvconstre  15799  dvconstss  15801  sgmmul  16116  pw1ndom3  17032