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

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

Proof of Theorem simp3rl
StepHypRef Expression
1 simprl 778 . 2 ((𝜒 ∧ (𝜑𝜓)) → 𝜑)
213ad2ant3 1158 1 ((𝜃𝜏 ∧ (𝜒 ∧ (𝜑𝜓))) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1100
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 198  df-an 385  df-3an 1102
This theorem is referenced by:  omeu  7896  hashbclem  13447  ntrivcvgmul  14849  tsmsxp  22165  tgqioo  22810  ovolunlem2  23473  plyadd  24181  plymul  24182  coeeu  24189  tghilberti2  25741  cvmlift2lem10  31611  nosupbnd1lem2  32170  btwnconn1lem1  32509  btwnconn1lem2  32510  btwnconn1lem12  32520  lplnexllnN  35338  2llnjN  35341  4atlem12b  35385  lplncvrlvol2  35389  lncmp  35557  cdlema2N  35566  cdlemc2  35967  cdleme11a  36035  cdleme22eALTN  36120  cdleme24  36127  cdleme27a  36142  cdleme27N  36144  cdleme28  36148  cdlemefs29bpre0N  36191  cdlemefs29bpre1N  36192  cdlemefs29cpre1N  36193  cdlemefs29clN  36194  cdlemefs32fvaN  36197  cdlemefs32fva1  36198  cdleme36m  36236  cdleme39a  36240  cdleme17d3  36271  cdleme50trn2  36326  cdlemg36  36489  cdlemj3  36598  cdlemkfid1N  36696  cdlemkid1  36697  cdlemk19ylem  36705  cdlemk19xlem  36717  dihlsscpre  37009  dihord4  37033  dihatlat  37109  mapdh9a  37564  jm2.27  38070
  Copyright terms: Public domain W3C validator