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  6031  suppfnss  6501  tfrlemibacc  6601  tfrlemibxssdm  6602  tfrlemibfn  6603  tfr1onlembacc  6617  tfr1onlembxssdm  6618  tfr1onlembfn  6619  tfrcllembacc  6630  tfrcllembxssdm  6631  tfrcllembfn  6632  elfir  7313  prloc  7865  prmuloc2  7941  ltntri  8462  eluzuzle  9947  xlesubadd  10303  elioc2  10356  elico2  10357  elicc2  10358  fseq1p1m1  10519  seq3f1olemp  10974  seq3f1oleml  10975  bcval5  11224  hashdifpr  11284  hashtpgim  11320  ccatswrd  11465  pfxccat3a  11533  isumss2  12186  tanaddap  12532  dvds2ln  12617  divalglemeunn  12714  divalglemex  12715  divalglemeuneg  12716  f1ovscpbl  13693  imasmnd2  13819  imasmnd  13820  grpsubadd  13953  grpaddsubass  13955  grpsubsub4  13958  grppnpcan2  13959  grpnpncan  13960  grpnnncan2  13962  imasgrp2  13973  imasgrp  13974  mulgnndir  14014  mulgnn0dir  14015  mulgnnass  14020  mulgnn0ass  14021  mulgass  14022  issubg2m  14052  qusgrp  14095  kerf1ghm  14137  cmn32  14198  cmn12  14200  abladdsub  14210  ablsubsub23  14220  prdssgrpd  14299  prdsmndd  14302  rngass  14346  imasrng  14363  srgdilem  14381  srgass  14383  ringdilem  14424  ringass  14428  ringrng  14449  imasring  14479  opprrng  14492  opprring  14494  mulgass3  14501  unitgrp  14533  dvrass  14556  dvrdir  14560  subrgunit  14657  issubrg2  14659  aprap  14708  lss1  14809  lsssn0  14817  islss3  14826  sralmod  14897  psrringfi  15209  restopnb  15419  icnpimaex  15449  cnptopresti  15476  psmettri  15568  isxmet2d  15586  xmettri  15610  metrtri  15615  xmetres2  15617  bldisj  15639  blss2ps  15644  blss2  15645  xmstri2  15708  mstri2  15709  xmstri  15710  mstri  15711  xmstri3  15712  mstri3  15713  msrtri  15714  comet  15737  bdbl  15741  xmetxp  15745  dvconst  15932  dvconstre  15934  dvconstss  15936  sgmmul  16302  pw1ndom3  17237