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

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

Proof of Theorem simp2rl
StepHypRef Expression
1 simprl 793 . 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  7421  omeu  7610  wemaplem3  8397  gruina  9584  4sqlem18  15590  vdwlem10  15618  mdetuni0  20346  mdetmul  20348  tsmsxp  21868  ax5seglem3  25711  btwnconn1lem1  31836  btwnconn1lem2  31837  btwnconn1lem3  31838  btwnconn1lem4  31839  btwnconn1lem12  31847  btwnconn1lem13  31848  linethru  31902  2llnjN  34333  2lplnja  34385  2lplnj  34386  cdlemblem  34559  dalaw  34652  pclfinN  34666  lhpmcvr4N  34792  lhp2atne  34800  lhp2at0ne  34802  cdlemb2  34807  cdlemd7  34971  cdleme01N  34988  cdleme02N  34989  cdleme0ex2N  34991  cdleme7aa  35009  cdleme7c  35012  cdleme7d  35013  cdleme7e  35014  cdleme7ga  35015  cdleme11a  35027  cdleme20k  35087  cdleme21d  35098  cdleme27cl  35134  cdlemefrs29bpre0  35164  cdlemefrs29cpre1  35166  cdlemefrs32fva  35168  cdlemefrs32fva1  35169  cdlemefr29exN  35170  cdlemefr32sn2aw  35172  cdlemefr31fv1  35179  cdlemefs32sn1aw  35182  cdlemefr44  35193  cdlemefr45e  35196  cdleme41sn3a  35201  cdleme35a  35216  cdleme35fnpq  35217  cdleme35b  35218  cdleme35c  35219  cdleme35d  35220  cdleme35e  35221  cdleme35f  35222  cdleme35sn3a  35227  cdleme42e  35247  cdleme42h  35250  cdleme42i  35251  cdleme17d2  35263  cdleme48fv  35267  cdleme48bw  35270  cdleme48b  35271  cdlemeg46c  35281  cdlemeg46ngfr  35286  cdleme48d  35303  cdlemg2kq  35370  cdlemg2m  35372  cdlemg7fvN  35392  cdlemg8a  35395  cdlemg11aq  35406  cdlemg10c  35407  cdlemg17a  35429  cdlemg31b0N  35462  cdlemg41  35486  cdlemh2  35584  cdlemi  35588  cdlemk21-2N  35659  dihmeetlem1N  36059  dihmeetlem13N  36088  expmordi  36992  iunrelexpmin1  37481
  Copyright terms: Public domain W3C validator