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

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

Proof of Theorem simp3rl
StepHypRef Expression
1 simprl 769 . 2 ((𝜒 ∧ (𝜑𝜓)) → 𝜑)
213ad2ant3 1135 1 ((𝜃𝜏 ∧ (𝜒 ∧ (𝜑𝜓))) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1087
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 206  df-an 397  df-3an 1089
This theorem is referenced by:  omeu  8528  hashbclem  14341  ntrivcvgmul  15779  tsmsxp  23490  tgqioo  24147  ovolunlem2  24846  plyadd  25562  plymul  25563  coeeu  25570  nosupbnd1lem2  27041  noinfbnd1lem2  27056  tghilberti2  27466  cvmlift2lem10  33775  btwnconn1lem1  34639  btwnconn1lem2  34640  btwnconn1lem12  34650  lplnexllnN  37994  2llnjN  37997  4atlem12b  38041  lplncvrlvol2  38045  lncmp  38213  cdlema2N  38222  cdlemc2  38622  cdleme11a  38690  cdleme22eALTN  38775  cdleme24  38782  cdleme27a  38797  cdleme27N  38799  cdleme28  38803  cdlemefs29bpre0N  38846  cdlemefs29bpre1N  38847  cdlemefs29cpre1N  38848  cdlemefs29clN  38849  cdlemefs32fvaN  38852  cdlemefs32fva1  38853  cdleme36m  38891  cdleme39a  38895  cdleme17d3  38926  cdleme50trn2  38981  cdlemg36  39144  cdlemj3  39253  cdlemkfid1N  39351  cdlemkid1  39352  cdlemk19ylem  39360  cdlemk19xlem  39372  dihlsscpre  39664  dihord4  39688  dihatlat  39764  mapdh9a  40219  jm2.27  41270
  Copyright terms: Public domain W3C validator