MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp3rl Structured version   Visualization version   GIF version

Theorem simp3rl 1313
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simp3rl ((𝜃𝜏 ∧ (𝜒 ∧ (𝜑𝜓))) → 𝜑)

Proof of Theorem simp3rl
StepHypRef Expression
1 simprl 811 . 2 ((𝜒 ∧ (𝜑𝜓)) → 𝜑)
213ad2ant3 1130 1 ((𝜃𝜏 ∧ (𝜒 ∧ (𝜑𝜓))) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1072
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 197  df-an 385  df-3an 1074
This theorem is referenced by:  omeu  7834  hashbclem  13428  ntrivcvgmul  14833  tsmsxp  22159  tgqioo  22804  ovolunlem2  23466  plyadd  24172  plymul  24173  coeeu  24180  tghilberti2  25732  cvmlift2lem10  31601  nosupbnd1lem2  32161  btwnconn1lem1  32500  btwnconn1lem2  32501  btwnconn1lem12  32511  lplnexllnN  35353  2llnjN  35356  4atlem12b  35400  lplncvrlvol2  35404  lncmp  35572  cdlema2N  35581  cdlemc2  35982  cdleme11a  36050  cdleme22eALTN  36135  cdleme24  36142  cdleme27a  36157  cdleme27N  36159  cdleme28  36163  cdlemefs29bpre0N  36206  cdlemefs29bpre1N  36207  cdlemefs29cpre1N  36208  cdlemefs29clN  36209  cdlemefs32fvaN  36212  cdlemefs32fva1  36213  cdleme36m  36251  cdleme39a  36255  cdleme17d3  36286  cdleme50trn2  36341  cdlemg36  36504  cdlemj3  36613  cdlemkfid1N  36711  cdlemkid1  36712  cdlemk19ylem  36720  cdlemk19xlem  36732  dihlsscpre  37025  dihord4  37049  dihatlat  37125  mapdh9a  37581  jm2.27  38077
  Copyright terms: Public domain W3C validator