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

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

Proof of Theorem simp3lr
StepHypRef Expression
1 simplr 809 . 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:  f1oiso2  6765  omeu  7834  ntrivcvgmul  14833  tsmsxp  22159  tgqioo  22804  ovolunlem2  23466  plyadd  24172  plymul  24173  coeeu  24180  tghilberti2  25732  nosupbnd1lem2  32161  btwnconn1lem2  32501  btwnconn1lem3  32502  btwnconn1lem4  32503  athgt  35245  2llnjN  35356  4atlem12b  35400  lncmp  35572  cdlema2N  35581  cdleme21ct  36119  cdleme24  36142  cdleme27a  36157  cdleme28  36163  cdleme42b  36268  cdlemf  36353  dihlsscpre  37025  dihord4  37049  dihord5apre  37053  pellex  37901  jm2.27  38077
 Copyright terms: Public domain W3C validator