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 770 . 2 ((𝜒 ∧ (𝜑𝜓)) → 𝜑)
213ad2ant3 1135 1 ((𝜃𝜏 ∧ (𝜒 ∧ (𝜑𝜓))) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  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 207  df-an 396  df-3an 1089
This theorem is referenced by:  omeu  8641  hashbclem  14501  ntrivcvgmul  15950  tsmsxp  24184  tgqioo  24841  ovolunlem2  25552  plyadd  26276  plymul  26277  coeeu  26284  nosupbnd1lem2  27772  noinfbnd1lem2  27787  tghilberti2  28664  cvmlift2lem10  35280  btwnconn1lem1  36051  btwnconn1lem2  36052  btwnconn1lem12  36062  lplnexllnN  39521  2llnjN  39524  4atlem12b  39568  lplncvrlvol2  39572  lncmp  39740  cdlema2N  39749  cdlemc2  40149  cdleme11a  40217  cdleme22eALTN  40302  cdleme24  40309  cdleme27a  40324  cdleme27N  40326  cdleme28  40330  cdlemefs29bpre0N  40373  cdlemefs29bpre1N  40374  cdlemefs29cpre1N  40375  cdlemefs29clN  40376  cdlemefs32fvaN  40379  cdlemefs32fva1  40380  cdleme36m  40418  cdleme39a  40422  cdleme17d3  40453  cdleme50trn2  40508  cdlemg36  40671  cdlemj3  40780  cdlemkfid1N  40878  cdlemkid1  40879  cdlemk19ylem  40887  cdlemk19xlem  40899  dihlsscpre  41191  dihord4  41215  dihatlat  41291  mapdh9a  41746  jm2.27  42965
  Copyright terms: Public domain W3C validator