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

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

Proof of Theorem simp3lr
StepHypRef Expression
1 simplr 788 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜓)
213ad2ant3 1077 1 ((𝜃𝜏 ∧ ((𝜑𝜓) ∧ 𝜒)) → 𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031 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 196  df-an 385  df-3an 1033 This theorem is referenced by:  f1oiso2  6502  omeu  7552  ntrivcvgmul  14473  tsmsxp  21768  tgqioo  22411  ovolunlem2  23073  plyadd  23777  plymul  23778  coeeu  23785  tghilberti2  25333  btwnconn1lem2  31365  btwnconn1lem3  31366  btwnconn1lem4  31367  athgt  33760  2llnjN  33871  4atlem12b  33915  lncmp  34087  cdlema2N  34096  cdleme21ct  34635  cdleme24  34658  cdleme27a  34673  cdleme28  34679  cdleme42b  34784  cdlemf  34869  dihlsscpre  35541  dihord4  35565  dihord5apre  35569  pellex  36417  jm2.27  36593
 Copyright terms: Public domain W3C validator