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

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

Proof of Theorem simp2rr
StepHypRef Expression
1 simprr 772 . 2 ((𝜒 ∧ (𝜑𝜓)) → 𝜓)
213ad2ant2 1131 1 ((𝜃 ∧ (𝜒 ∧ (𝜑𝜓)) ∧ 𝜏) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1084
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 210  df-an 400  df-3an 1086
This theorem is referenced by:  tfrlem5  7991  omeu  8186  gruina  10217  4sqlem18  16275  vdwlem10  16303  mdetuni0  21205  mdetmul  21207  tsmsxp  22738  ax5seglem3  26703  fpr3g  33129  btwnconn1lem1  33555  btwnconn1lem3  33557  btwnconn1lem4  33558  btwnconn1lem5  33559  btwnconn1lem6  33560  btwnconn1lem7  33561  btwnconn1lem12  33566  linethru  33621  2llnjN  36743  2lplnja  36795  2lplnj  36796  cdlemblem  36969  dalaw  37062  pclfinN  37076  lhpmcvr4N  37202  cdlemb2  37217  cdleme01N  37397  cdleme0ex2N  37400  cdleme7c  37421  cdlemefrs29bpre0  37572  cdlemefrs29cpre1  37574  cdlemefrs32fva1  37577  cdlemefs32sn1aw  37590  cdleme41sn3a  37609  cdleme48fv  37675  cdlemk21-2N  38067  dihmeetlem13N  38495  pellex  39573  lmhmfgsplit  39827  iunrelexpmin1  40190
  Copyright terms: Public domain W3C validator