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

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

Proof of Theorem simp2rr
StepHypRef Expression
1 simprr 791 . 2 ((𝜒 ∧ (𝜑𝜓)) → 𝜓)
213ad2ant2 1170 1 ((𝜃 ∧ (𝜒 ∧ (𝜑𝜓)) ∧ 𝜏) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 386  w3a 1113
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 199  df-an 387  df-3an 1115
This theorem is referenced by:  tfrlem5  7742  omeu  7932  gruina  9955  4sqlem18  16037  vdwlem10  16065  mdetuni0  20795  mdetmul  20797  tsmsxp  22328  ax5seglem3  26230  btwnconn1lem1  32733  btwnconn1lem3  32735  btwnconn1lem4  32736  btwnconn1lem5  32737  btwnconn1lem6  32738  btwnconn1lem7  32739  btwnconn1lem12  32744  linethru  32799  2llnjN  35642  2lplnja  35694  2lplnj  35695  cdlemblem  35868  dalaw  35961  pclfinN  35975  lhpmcvr4N  36101  cdlemb2  36116  cdleme01N  36296  cdleme0ex2N  36299  cdleme7c  36320  cdlemefrs29bpre0  36471  cdlemefrs29cpre1  36473  cdlemefrs32fva1  36476  cdlemefs32sn1aw  36489  cdleme41sn3a  36508  cdleme48fv  36574  cdlemk21-2N  36966  dihmeetlem13N  37394  pellex  38243  lmhmfgsplit  38499  iunrelexpmin1  38841
  Copyright terms: Public domain W3C validator