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

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

Proof of Theorem simp2rr
StepHypRef Expression
1 simprr 769 . 2 ((𝜒 ∧ (𝜑𝜓)) → 𝜓)
213ad2ant2 1126 1 ((𝜃 ∧ (𝜒 ∧ (𝜑𝜓)) ∧ 𝜏) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1079
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 208  df-an 397  df-3an 1081
This theorem is referenced by:  tfrlem5  8005  omeu  8200  gruina  10228  4sqlem18  16286  vdwlem10  16314  mdetuni0  21158  mdetmul  21160  tsmsxp  22690  ax5seglem3  26644  fpr3g  33019  btwnconn1lem1  33445  btwnconn1lem3  33447  btwnconn1lem4  33448  btwnconn1lem5  33449  btwnconn1lem6  33450  btwnconn1lem7  33451  btwnconn1lem12  33456  linethru  33511  2llnjN  36583  2lplnja  36635  2lplnj  36636  cdlemblem  36809  dalaw  36902  pclfinN  36916  lhpmcvr4N  37042  cdlemb2  37057  cdleme01N  37237  cdleme0ex2N  37240  cdleme7c  37261  cdlemefrs29bpre0  37412  cdlemefrs29cpre1  37414  cdlemefrs32fva1  37417  cdlemefs32sn1aw  37430  cdleme41sn3a  37449  cdleme48fv  37515  cdlemk21-2N  37907  dihmeetlem13N  38335  pellex  39310  lmhmfgsplit  39564  iunrelexpmin1  39931
  Copyright terms: Public domain W3C validator