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  5997  suppfnss  6459  tfrlemibacc  6559  tfrlemibxssdm  6560  tfrlemibfn  6561  tfr1onlembacc  6575  tfr1onlembxssdm  6576  tfr1onlembfn  6577  tfrcllembacc  6588  tfrcllembxssdm  6589  tfrcllembfn  6590  elfir  7262  prloc  7811  prmuloc2  7887  ltntri  8406  eluzuzle  9868  xlesubadd  10222  elioc2  10275  elico2  10276  elicc2  10277  fseq1p1m1  10435  seq3f1olemp  10884  seq3f1oleml  10885  bcval5  11133  hashdifpr  11193  hashtpgim  11225  ccatswrd  11370  pfxccat3a  11438  isumss2  12087  tanaddap  12433  dvds2ln  12518  divalglemeunn  12615  divalglemex  12616  divalglemeuneg  12617  f1ovscpbl  13546  prdssgrpd  13649  prdsmndd  13682  imasmnd2  13686  imasmnd  13687  grpsubadd  13822  grpaddsubass  13824  grpsubsub4  13827  grppnpcan2  13828  grpnpncan  13829  grpnnncan2  13831  imasgrp2  13848  imasgrp  13849  mulgnndir  13889  mulgnn0dir  13890  mulgnnass  13895  mulgnn0ass  13896  mulgass  13897  issubg2m  13927  qusgrp  13970  kerf1ghm  14012  cmn32  14042  cmn12  14044  abladdsub  14053  ablsubsub23  14063  rngass  14104  imasrng  14121  srgdilem  14134  srgass  14136  ringdilem  14177  ringass  14181  ringrng  14201  imasring  14229  opprrng  14242  opprring  14244  mulgass3  14251  unitgrp  14283  dvrass  14306  dvrdir  14310  subrgunit  14407  issubrg2  14409  aprap  14458  lss1  14559  lsssn0  14567  islss3  14576  sralmod  14647  restopnb  15095  icnpimaex  15125  cnptopresti  15152  psmettri  15244  isxmet2d  15262  xmettri  15286  metrtri  15291  xmetres2  15293  bldisj  15315  blss2ps  15320  blss2  15321  xmstri2  15384  mstri2  15385  xmstri  15386  mstri  15387  xmstri3  15388  mstri3  15389  msrtri  15390  comet  15413  bdbl  15417  xmetxp  15421  dvconst  15608  dvconstre  15610  dvconstss  15612  sgmmul  15913  pw1ndom3  16813