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

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

Proof of Theorem simp2rr
StepHypRef Expression
1 simprr 811 . 2 ((𝜒 ∧ (𝜑𝜓)) → 𝜓)
213ad2ant2 1103 1 ((𝜃 ∧ (𝜒 ∧ (𝜑𝜓)) ∧ 𝜏) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1054
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 1056
This theorem is referenced by:  tfrlem5  7521  omeu  7710  gruina  9678  4sqlem18  15713  vdwlem10  15741  mdetuni0  20475  mdetmul  20477  tsmsxp  22005  ax5seglem3  25856  btwnconn1lem1  32319  btwnconn1lem3  32321  btwnconn1lem4  32322  btwnconn1lem5  32323  btwnconn1lem6  32324  btwnconn1lem7  32325  btwnconn1lem12  32330  linethru  32385  2llnjN  35171  2lplnja  35223  2lplnj  35224  cdlemblem  35397  dalaw  35490  pclfinN  35504  lhpmcvr4N  35630  cdlemb2  35645  cdleme01N  35826  cdleme0ex2N  35829  cdleme7c  35850  cdlemefrs29bpre0  36001  cdlemefrs29cpre1  36003  cdlemefrs32fva1  36006  cdlemefs32sn1aw  36019  cdleme41sn3a  36038  cdleme48fv  36104  cdlemk21-2N  36496  dihmeetlem13N  36925  pellex  37716  lmhmfgsplit  37973  iunrelexpmin1  38317
  Copyright terms: Public domain W3C validator