Theorem simpr3 1010

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

Assertion

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

Proof of Theorem simpr3

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

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

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 985

This theorem is referenced by:  simplr3  1046  simprr3  1052  simp1r3  1100  simp2r3  1106  simp3r3  1112  3anandis  1362  isopolem  5919  tfrlemibacc  6442  tfrlemibxssdm  6443  tfrlemibfn  6444  tfr1onlembacc  6458  tfr1onlembxssdm  6459  tfr1onlembfn  6460  tfrcllembacc  6471  tfrcllembxssdm  6472  tfrcllembfn  6473  elfir  7108  prloc  7646  prmuloc2  7722  ltntri  8242  eluzuzle  9698  xlesubadd  10047  elioc2  10100  elico2  10101  elicc2  10102  fseq1p1m1  10258  seq3f1olemp  10704  seq3f1oleml  10705  bcval5  10952  hashdifpr  11009  ccatswrd  11168  pfxccat3a  11236  isumss2  11870  tanaddap  12216  dvds2ln  12301  divalglemeunn  12398  divalglemex  12399  divalglemeuneg  12400  f1ovscpbl  13311  prdssgrpd  13414  prdsmndd  13447  imasmnd2  13451  imasmnd  13452  grpsubadd  13587  grpaddsubass  13589  grpsubsub4  13592  grppnpcan2  13593  grpnpncan  13594  grpnnncan2  13596  imasgrp2  13613  imasgrp  13614  mulgnndir  13654  mulgnn0dir  13655  mulgnnass  13660  mulgnn0ass  13661  mulgass  13662  issubg2m  13692  qusgrp  13735  kerf1ghm  13777  cmn32  13807  cmn12  13809  abladdsub  13818  ablsubsub23  13828  rngass  13868  imasrng  13885  srgdilem  13898  srgass  13900  ringdilem  13941  ringass  13945  ringrng  13965  imasring  13993  opprrng  14006  opprring  14008  mulgass3  14014  unitgrp  14045  dvrass  14068  dvrdir  14072  subrgunit  14168  issubrg2  14170  aprap  14215  lss1  14291  lsssn0  14299  islss3  14308  sralmod  14379  restopnb  14820  icnpimaex  14850  cnptopresti  14877  psmettri  14969  isxmet2d  14987  xmettri  15011  metrtri  15016  xmetres2  15018  bldisj  15040  blss2ps  15045  blss2  15046  xmstri2  15109  mstri2  15110  xmstri  15111  mstri  15112  xmstri3  15113  mstri3  15114  msrtri  15115  comet  15138  bdbl  15142  xmetxp  15146  dvconst  15333  dvconstre  15335  dvconstss  15337  sgmmul  15635