Theorem simpr3 1032

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

Assertion

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

Proof of Theorem simpr3

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

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

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 1007

This theorem is referenced by:  simplr3  1068  simprr3  1074  simp1r3  1122  simp2r3  1128  simp3r3  1134  3anandis  1384  isopolem  6001  suppfnss  6470  tfrlemibacc  6570  tfrlemibxssdm  6571  tfrlemibfn  6572  tfr1onlembacc  6586  tfr1onlembxssdm  6587  tfr1onlembfn  6588  tfrcllembacc  6599  tfrcllembxssdm  6600  tfrcllembfn  6601  elfir  7273  prloc  7822  prmuloc2  7898  ltntri  8418  eluzuzle  9883  xlesubadd  10238  elioc2  10291  elico2  10292  elicc2  10293  fseq1p1m1  10453  seq3f1olemp  10904  seq3f1oleml  10905  bcval5  11153  hashdifpr  11213  hashtpgim  11245  ccatswrd  11390  pfxccat3a  11458  isumss2  12107  tanaddap  12453  dvds2ln  12538  divalglemeunn  12635  divalglemex  12636  divalglemeuneg  12637  f1ovscpbl  13579  imasmnd2  13710  imasmnd  13711  grpsubadd  13846  grpaddsubass  13848  grpsubsub4  13851  grppnpcan2  13852  grpnpncan  13853  grpnnncan2  13855  imasgrp2  13866  imasgrp  13867  mulgnndir  13907  mulgnn0dir  13908  mulgnnass  13913  mulgnn0ass  13914  mulgass  13915  issubg2m  13945  qusgrp  13988  kerf1ghm  14030  cmn32  14060  cmn12  14062  abladdsub  14071  ablsubsub23  14081  prdssgrpd  14136  prdsmndd  14139  rngass  14181  imasrng  14198  srgdilem  14215  srgass  14217  ringdilem  14258  ringass  14262  ringrng  14282  imasring  14310  opprrng  14323  opprring  14325  mulgass3  14332  unitgrp  14364  dvrass  14387  dvrdir  14391  subrgunit  14488  issubrg2  14490  aprap  14539  lss1  14639  lsssn0  14647  islss3  14656  sralmod  14727  restopnb  15175  icnpimaex  15205  cnptopresti  15232  psmettri  15324  isxmet2d  15342  xmettri  15366  metrtri  15371  xmetres2  15373  bldisj  15395  blss2ps  15400  blss2  15401  xmstri2  15464  mstri2  15465  xmstri  15466  mstri  15467  xmstri3  15468  mstri3  15469  msrtri  15470  comet  15493  bdbl  15497  xmetxp  15501  dvconst  15688  dvconstre  15690  dvconstss  15692  sgmmul  15993  pw1ndom3  16903