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

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

Proof of Theorem simp2rr
StepHypRef Expression
1 simprr 795 . 2 ((𝜒 ∧ (𝜑𝜓)) → 𝜓)
213ad2ant2 1081 1 ((𝜃 ∧ (𝜒 ∧ (𝜑𝜓)) ∧ 𝜏) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036
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 386  df-3an 1038
This theorem is referenced by:  tfrlem5  7428  omeu  7617  gruina  9592  4sqlem18  15601  vdwlem10  15629  mdetuni0  20359  mdetmul  20361  tsmsxp  21881  ax5seglem3  25728  btwnconn1lem1  31871  btwnconn1lem3  31873  btwnconn1lem4  31874  btwnconn1lem5  31875  btwnconn1lem6  31876  btwnconn1lem7  31877  btwnconn1lem12  31882  linethru  31937  2llnjN  34368  2lplnja  34420  2lplnj  34421  cdlemblem  34594  dalaw  34687  pclfinN  34701  lhpmcvr4N  34827  cdlemb2  34842  cdleme01N  35023  cdleme0ex2N  35026  cdleme7c  35047  cdlemefrs29bpre0  35199  cdlemefrs29cpre1  35201  cdlemefrs32fva1  35204  cdlemefs32sn1aw  35217  cdleme41sn3a  35236  cdleme48fv  35302  cdlemk21-2N  35694  dihmeetlem13N  36123  pellex  36914  lmhmfgsplit  37171  iunrelexpmin1  37516
  Copyright terms: Public domain W3C validator