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

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

Proof of Theorem simp3lr
StepHypRef Expression
1 simplr 792 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜓)
213ad2ant3 1083 1 ((𝜃𝜏 ∧ ((𝜑𝜓) ∧ 𝜒)) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1037
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 386  df-3an 1039
This theorem is referenced by:  f1oiso2  6599  omeu  7662  ntrivcvgmul  14628  tsmsxp  21952  tgqioo  22597  ovolunlem2  23260  plyadd  23967  plymul  23968  coeeu  23975  tghilberti2  25527  nosupbnd1lem2  31839  btwnconn1lem2  32179  btwnconn1lem3  32180  btwnconn1lem4  32181  athgt  34568  2llnjN  34679  4atlem12b  34723  lncmp  34895  cdlema2N  34904  cdleme21ct  35443  cdleme24  35466  cdleme27a  35481  cdleme28  35487  cdleme42b  35592  cdlemf  35677  dihlsscpre  36349  dihord4  36373  dihord5apre  36377  pellex  37225  jm2.27  37401
  Copyright terms: Public domain W3C validator