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  5963  tfrlemibacc  6492  tfrlemibxssdm  6493  tfrlemibfn  6494  tfr1onlembacc  6508  tfr1onlembxssdm  6509  tfr1onlembfn  6510  tfrcllembacc  6521  tfrcllembxssdm  6522  tfrcllembfn  6523  elfir  7172  prloc  7711  prmuloc2  7787  ltntri  8307  eluzuzle  9764  xlesubadd  10118  elioc2  10171  elico2  10172  elicc2  10173  fseq1p1m1  10329  seq3f1olemp  10778  seq3f1oleml  10779  bcval5  11026  hashdifpr  11085  ccatswrd  11252  pfxccat3a  11320  isumss2  11956  tanaddap  12302  dvds2ln  12387  divalglemeunn  12484  divalglemex  12485  divalglemeuneg  12486  f1ovscpbl  13397  prdssgrpd  13500  prdsmndd  13533  imasmnd2  13537  imasmnd  13538  grpsubadd  13673  grpaddsubass  13675  grpsubsub4  13678  grppnpcan2  13679  grpnpncan  13680  grpnnncan2  13682  imasgrp2  13699  imasgrp  13700  mulgnndir  13740  mulgnn0dir  13741  mulgnnass  13746  mulgnn0ass  13747  mulgass  13748  issubg2m  13778  qusgrp  13821  kerf1ghm  13863  cmn32  13893  cmn12  13895  abladdsub  13904  ablsubsub23  13914  rngass  13955  imasrng  13972  srgdilem  13985  srgass  13987  ringdilem  14028  ringass  14032  ringrng  14052  imasring  14080  opprrng  14093  opprring  14095  mulgass3  14101  unitgrp  14133  dvrass  14156  dvrdir  14160  subrgunit  14256  issubrg2  14258  aprap  14303  lss1  14379  lsssn0  14387  islss3  14396  sralmod  14467  restopnb  14908  icnpimaex  14938  cnptopresti  14965  psmettri  15057  isxmet2d  15075  xmettri  15099  metrtri  15104  xmetres2  15106  bldisj  15128  blss2ps  15133  blss2  15134  xmstri2  15197  mstri2  15198  xmstri  15199  mstri  15200  xmstri3  15201  mstri3  15202  msrtri  15203  comet  15226  bdbl  15230  xmetxp  15234  dvconst  15421  dvconstre  15423  dvconstss  15425  sgmmul  15723  pw1ndom3  16610