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  5994  suppfnss  6456  tfrlemibacc  6556  tfrlemibxssdm  6557  tfrlemibfn  6558  tfr1onlembacc  6572  tfr1onlembxssdm  6573  tfr1onlembfn  6574  tfrcllembacc  6585  tfrcllembxssdm  6586  tfrcllembfn  6587  elfir  7259  prloc  7802  prmuloc2  7878  ltntri  8397  eluzuzle  9858  xlesubadd  10212  elioc2  10265  elico2  10266  elicc2  10267  fseq1p1m1  10424  seq3f1olemp  10873  seq3f1oleml  10874  bcval5  11121  hashdifpr  11180  hashtpgim  11210  ccatswrd  11355  pfxccat3a  11423  isumss2  12072  tanaddap  12418  dvds2ln  12503  divalglemeunn  12600  divalglemex  12601  divalglemeuneg  12602  f1ovscpbl  13514  prdssgrpd  13617  prdsmndd  13650  imasmnd2  13654  imasmnd  13655  grpsubadd  13790  grpaddsubass  13792  grpsubsub4  13795  grppnpcan2  13796  grpnpncan  13797  grpnnncan2  13799  imasgrp2  13816  imasgrp  13817  mulgnndir  13857  mulgnn0dir  13858  mulgnnass  13863  mulgnn0ass  13864  mulgass  13865  issubg2m  13895  qusgrp  13938  kerf1ghm  13980  cmn32  14010  cmn12  14012  abladdsub  14021  ablsubsub23  14031  rngass  14072  imasrng  14089  srgdilem  14102  srgass  14104  ringdilem  14145  ringass  14149  ringrng  14169  imasring  14197  opprrng  14210  opprring  14212  mulgass3  14218  unitgrp  14250  dvrass  14273  dvrdir  14277  subrgunit  14373  issubrg2  14375  aprap  14421  lss1  14497  lsssn0  14505  islss3  14514  sralmod  14585  restopnb  15033  icnpimaex  15063  cnptopresti  15090  psmettri  15182  isxmet2d  15200  xmettri  15224  metrtri  15229  xmetres2  15231  bldisj  15253  blss2ps  15258  blss2  15259  xmstri2  15322  mstri2  15323  xmstri  15324  mstri  15325  xmstri3  15326  mstri3  15327  msrtri  15328  comet  15351  bdbl  15355  xmetxp  15359  dvconst  15546  dvconstre  15548  dvconstss  15550  sgmmul  15851  pw1ndom3  16751