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

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

Proof of Theorem simp2rl
StepHypRef Expression
1 simprl 770 . 2 ((𝜒 ∧ (𝜑𝜓)) → 𝜑)
213ad2ant2 1135 1 ((𝜃 ∧ (𝜒 ∧ (𝜑𝜓)) ∧ 𝜏) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  w3a 1088
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 206  df-an 398  df-3an 1090
This theorem is referenced by:  tfrlem5  8330  omeu  8536  wemaplem3  9492  gruina  10762  expmordi  14081  4sqlem18  16842  vdwlem10  16870  mdetuni0  21993  mdetmul  21995  tsmsxp  23529  ax5seglem3  27929  btwnconn1lem1  34725  btwnconn1lem2  34726  btwnconn1lem3  34727  btwnconn1lem4  34728  btwnconn1lem12  34736  btwnconn1lem13  34737  linethru  34791  2llnjN  38080  2lplnja  38132  2lplnj  38133  cdlemblem  38306  dalaw  38399  pclfinN  38413  lhpmcvr4N  38539  lhp2atne  38547  lhp2at0ne  38549  cdlemb2  38554  cdlemd7  38717  cdleme01N  38734  cdleme02N  38735  cdleme0ex2N  38737  cdleme7aa  38755  cdleme7c  38758  cdleme7d  38759  cdleme7e  38760  cdleme7ga  38761  cdleme11a  38773  cdleme20k  38832  cdleme21d  38843  cdleme27cl  38879  cdlemefrs29bpre0  38909  cdlemefrs29cpre1  38911  cdlemefrs32fva  38913  cdlemefrs32fva1  38914  cdlemefr29exN  38915  cdlemefr32sn2aw  38917  cdlemefr31fv1  38924  cdlemefs32sn1aw  38927  cdlemefr44  38938  cdlemefr45e  38941  cdleme41sn3a  38946  cdleme35a  38961  cdleme35fnpq  38962  cdleme35b  38963  cdleme35c  38964  cdleme35d  38965  cdleme35e  38966  cdleme35f  38967  cdleme35sn3a  38972  cdleme42e  38992  cdleme42h  38995  cdleme42i  38996  cdleme17d2  39008  cdleme48fv  39012  cdleme48bw  39015  cdleme48b  39016  cdlemeg46c  39026  cdlemeg46ngfr  39031  cdleme48d  39048  cdlemg2kq  39115  cdlemg2m  39117  cdlemg7fvN  39137  cdlemg8a  39140  cdlemg11aq  39151  cdlemg10c  39152  cdlemg17a  39174  cdlemg31b0N  39207  cdlemg41  39231  cdlemh2  39329  cdlemi  39333  cdlemk21-2N  39404  dihmeetlem1N  39803  dihmeetlem13N  39832  iunrelexpmin1  42072
  Copyright terms: Public domain W3C validator