Theorem simpr3 1031

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

Assertion

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

Proof of Theorem simpr3

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

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

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 1006

This theorem is referenced by:  simplr3  1067  simprr3  1073  simp1r3  1121  simp2r3  1127  simp3r3  1133  3anandis  1383  isopolem  5968  tfrlemibacc  6497  tfrlemibxssdm  6498  tfrlemibfn  6499  tfr1onlembacc  6513  tfr1onlembxssdm  6514  tfr1onlembfn  6515  tfrcllembacc  6526  tfrcllembxssdm  6527  tfrcllembfn  6528  elfir  7177  prloc  7716  prmuloc2  7792  ltntri  8312  eluzuzle  9769  xlesubadd  10123  elioc2  10176  elico2  10177  elicc2  10178  fseq1p1m1  10334  seq3f1olemp  10783  seq3f1oleml  10784  bcval5  11031  hashdifpr  11090  hashtpgim  11115  ccatswrd  11260  pfxccat3a  11328  isumss2  11977  tanaddap  12323  dvds2ln  12408  divalglemeunn  12505  divalglemex  12506  divalglemeuneg  12507  f1ovscpbl  13418  prdssgrpd  13521  prdsmndd  13554  imasmnd2  13558  imasmnd  13559  grpsubadd  13694  grpaddsubass  13696  grpsubsub4  13699  grppnpcan2  13700  grpnpncan  13701  grpnnncan2  13703  imasgrp2  13720  imasgrp  13721  mulgnndir  13761  mulgnn0dir  13762  mulgnnass  13767  mulgnn0ass  13768  mulgass  13769  issubg2m  13799  qusgrp  13842  kerf1ghm  13884  cmn32  13914  cmn12  13916  abladdsub  13925  ablsubsub23  13935  rngass  13976  imasrng  13993  srgdilem  14006  srgass  14008  ringdilem  14049  ringass  14053  ringrng  14073  imasring  14101  opprrng  14114  opprring  14116  mulgass3  14122  unitgrp  14154  dvrass  14177  dvrdir  14181  subrgunit  14277  issubrg2  14279  aprap  14324  lss1  14400  lsssn0  14408  islss3  14417  sralmod  14488  restopnb  14934  icnpimaex  14964  cnptopresti  14991  psmettri  15083  isxmet2d  15101  xmettri  15125  metrtri  15130  xmetres2  15132  bldisj  15154  blss2ps  15159  blss2  15160  xmstri2  15223  mstri2  15224  xmstri  15225  mstri  15226  xmstri3  15227  mstri3  15228  msrtri  15229  comet  15252  bdbl  15256  xmetxp  15260  dvconst  15447  dvconstre  15449  dvconstss  15451  sgmmul  15749  pw1ndom3  16649