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

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

Proof of Theorem simp2rl
StepHypRef Expression
1 simprl 811 . 2 ((𝜒 ∧ (𝜑𝜓)) → 𝜑)
213ad2ant2 1129 1 ((𝜃 ∧ (𝜒 ∧ (𝜑𝜓)) ∧ 𝜏) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1072
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 1074
This theorem is referenced by:  tfrlem5  7646  omeu  7836  wemaplem3  8620  gruina  9852  4sqlem18  15888  vdwlem10  15916  mdetuni0  20649  mdetmul  20651  tsmsxp  22179  ax5seglem3  26031  btwnconn1lem1  32521  btwnconn1lem2  32522  btwnconn1lem3  32523  btwnconn1lem4  32524  btwnconn1lem12  32532  btwnconn1lem13  32533  linethru  32587  2llnjN  35374  2lplnja  35426  2lplnj  35427  cdlemblem  35600  dalaw  35693  pclfinN  35707  lhpmcvr4N  35833  lhp2atne  35841  lhp2at0ne  35843  cdlemb2  35848  cdlemd7  36012  cdleme01N  36029  cdleme02N  36030  cdleme0ex2N  36032  cdleme7aa  36050  cdleme7c  36053  cdleme7d  36054  cdleme7e  36055  cdleme7ga  36056  cdleme11a  36068  cdleme20k  36127  cdleme21d  36138  cdleme27cl  36174  cdlemefrs29bpre0  36204  cdlemefrs29cpre1  36206  cdlemefrs32fva  36208  cdlemefrs32fva1  36209  cdlemefr29exN  36210  cdlemefr32sn2aw  36212  cdlemefr31fv1  36219  cdlemefs32sn1aw  36222  cdlemefr44  36233  cdlemefr45e  36236  cdleme41sn3a  36241  cdleme35a  36256  cdleme35fnpq  36257  cdleme35b  36258  cdleme35c  36259  cdleme35d  36260  cdleme35e  36261  cdleme35f  36262  cdleme35sn3a  36267  cdleme42e  36287  cdleme42h  36290  cdleme42i  36291  cdleme17d2  36303  cdleme48fv  36307  cdleme48bw  36310  cdleme48b  36311  cdlemeg46c  36321  cdlemeg46ngfr  36326  cdleme48d  36343  cdlemg2kq  36410  cdlemg2m  36412  cdlemg7fvN  36432  cdlemg8a  36435  cdlemg11aq  36446  cdlemg10c  36447  cdlemg17a  36469  cdlemg31b0N  36502  cdlemg41  36526  cdlemh2  36624  cdlemi  36628  cdlemk21-2N  36699  dihmeetlem1N  37099  dihmeetlem13N  37128  expmordi  38032  iunrelexpmin1  38520
  Copyright terms: Public domain W3C validator