Theorem simpr3 1029

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

Assertion

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

Proof of Theorem simpr3

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

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

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 1004

This theorem is referenced by:  simplr3  1065  simprr3  1071  simp1r3  1119  simp2r3  1125  simp3r3  1131  3anandis  1381  isopolem  5958  tfrlemibacc  6487  tfrlemibxssdm  6488  tfrlemibfn  6489  tfr1onlembacc  6503  tfr1onlembxssdm  6504  tfr1onlembfn  6505  tfrcllembacc  6516  tfrcllembxssdm  6517  tfrcllembfn  6518  elfir  7166  prloc  7704  prmuloc2  7780  ltntri  8300  eluzuzle  9757  xlesubadd  10111  elioc2  10164  elico2  10165  elicc2  10166  fseq1p1m1  10322  seq3f1olemp  10770  seq3f1oleml  10771  bcval5  11018  hashdifpr  11077  ccatswrd  11244  pfxccat3a  11312  isumss2  11947  tanaddap  12293  dvds2ln  12378  divalglemeunn  12475  divalglemex  12476  divalglemeuneg  12477  f1ovscpbl  13388  prdssgrpd  13491  prdsmndd  13524  imasmnd2  13528  imasmnd  13529  grpsubadd  13664  grpaddsubass  13666  grpsubsub4  13669  grppnpcan2  13670  grpnpncan  13671  grpnnncan2  13673  imasgrp2  13690  imasgrp  13691  mulgnndir  13731  mulgnn0dir  13732  mulgnnass  13737  mulgnn0ass  13738  mulgass  13739  issubg2m  13769  qusgrp  13812  kerf1ghm  13854  cmn32  13884  cmn12  13886  abladdsub  13895  ablsubsub23  13905  rngass  13945  imasrng  13962  srgdilem  13975  srgass  13977  ringdilem  14018  ringass  14022  ringrng  14042  imasring  14070  opprrng  14083  opprring  14085  mulgass3  14091  unitgrp  14123  dvrass  14146  dvrdir  14150  subrgunit  14246  issubrg2  14248  aprap  14293  lss1  14369  lsssn0  14377  islss3  14386  sralmod  14457  restopnb  14898  icnpimaex  14928  cnptopresti  14955  psmettri  15047  isxmet2d  15065  xmettri  15089  metrtri  15094  xmetres2  15096  bldisj  15118  blss2ps  15123  blss2  15124  xmstri2  15187  mstri2  15188  xmstri  15189  mstri  15190  xmstri3  15191  mstri3  15192  msrtri  15193  comet  15216  bdbl  15220  xmetxp  15224  dvconst  15411  dvconstre  15413  dvconstss  15415  sgmmul  15713  pw1ndom3  16539