Theorem simpr3 1008

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

Assertion

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

Proof of Theorem simpr3

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

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

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 983

This theorem is referenced by:  simplr3  1044  simprr3  1050  simp1r3  1098  simp2r3  1104  simp3r3  1110  3anandis  1360  isopolem  5898  tfrlemibacc  6419  tfrlemibxssdm  6420  tfrlemibfn  6421  tfr1onlembacc  6435  tfr1onlembxssdm  6436  tfr1onlembfn  6437  tfrcllembacc  6448  tfrcllembxssdm  6449  tfrcllembfn  6450  elfir  7082  prloc  7611  prmuloc2  7687  ltntri  8207  eluzuzle  9663  xlesubadd  10012  elioc2  10065  elico2  10066  elicc2  10067  fseq1p1m1  10223  seq3f1olemp  10667  seq3f1oleml  10668  bcval5  10915  hashdifpr  10972  ccatswrd  11131  isumss2  11748  tanaddap  12094  dvds2ln  12179  divalglemeunn  12276  divalglemex  12277  divalglemeuneg  12278  f1ovscpbl  13188  prdssgrpd  13291  prdsmndd  13324  imasmnd2  13328  imasmnd  13329  grpsubadd  13464  grpaddsubass  13466  grpsubsub4  13469  grppnpcan2  13470  grpnpncan  13471  grpnnncan2  13473  imasgrp2  13490  imasgrp  13491  mulgnndir  13531  mulgnn0dir  13532  mulgnnass  13537  mulgnn0ass  13538  mulgass  13539  issubg2m  13569  qusgrp  13612  kerf1ghm  13654  cmn32  13684  cmn12  13686  abladdsub  13695  ablsubsub23  13705  rngass  13745  imasrng  13762  srgdilem  13775  srgass  13777  ringdilem  13818  ringass  13822  ringrng  13842  imasring  13870  opprrng  13883  opprring  13885  mulgass3  13891  unitgrp  13922  dvrass  13945  dvrdir  13949  subrgunit  14045  issubrg2  14047  aprap  14092  lss1  14168  lsssn0  14176  islss3  14185  sralmod  14256  restopnb  14697  icnpimaex  14727  cnptopresti  14754  psmettri  14846  isxmet2d  14864  xmettri  14888  metrtri  14893  xmetres2  14895  bldisj  14917  blss2ps  14922  blss2  14923  xmstri2  14986  mstri2  14987  xmstri  14988  mstri  14989  xmstri3  14990  mstri3  14991  msrtri  14992  comet  15015  bdbl  15019  xmetxp  15023  dvconst  15210  dvconstre  15212  dvconstss  15214  sgmmul  15512