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

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

Proof of Theorem simp2rl
StepHypRef Expression
1 simprl 767 . 2 ((𝜒 ∧ (𝜑𝜓)) → 𝜑)
213ad2ant2 1126 1 ((𝜃 ∧ (𝜒 ∧ (𝜑𝜓)) ∧ 𝜏) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1079
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 208  df-an 397  df-3an 1081
This theorem is referenced by:  tfrlem5  8005  omeu  8200  wemaplem3  9000  gruina  10228  expmordi  13519  4sqlem18  16286  vdwlem10  16314  mdetuni0  21158  mdetmul  21160  tsmsxp  22690  ax5seglem3  26644  btwnconn1lem1  33445  btwnconn1lem2  33446  btwnconn1lem3  33447  btwnconn1lem4  33448  btwnconn1lem12  33456  btwnconn1lem13  33457  linethru  33511  2llnjN  36583  2lplnja  36635  2lplnj  36636  cdlemblem  36809  dalaw  36902  pclfinN  36916  lhpmcvr4N  37042  lhp2atne  37050  lhp2at0ne  37052  cdlemb2  37057  cdlemd7  37220  cdleme01N  37237  cdleme02N  37238  cdleme0ex2N  37240  cdleme7aa  37258  cdleme7c  37261  cdleme7d  37262  cdleme7e  37263  cdleme7ga  37264  cdleme11a  37276  cdleme20k  37335  cdleme21d  37346  cdleme27cl  37382  cdlemefrs29bpre0  37412  cdlemefrs29cpre1  37414  cdlemefrs32fva  37416  cdlemefrs32fva1  37417  cdlemefr29exN  37418  cdlemefr32sn2aw  37420  cdlemefr31fv1  37427  cdlemefs32sn1aw  37430  cdlemefr44  37441  cdlemefr45e  37444  cdleme41sn3a  37449  cdleme35a  37464  cdleme35fnpq  37465  cdleme35b  37466  cdleme35c  37467  cdleme35d  37468  cdleme35e  37469  cdleme35f  37470  cdleme35sn3a  37475  cdleme42e  37495  cdleme42h  37498  cdleme42i  37499  cdleme17d2  37511  cdleme48fv  37515  cdleme48bw  37518  cdleme48b  37519  cdlemeg46c  37529  cdlemeg46ngfr  37534  cdleme48d  37551  cdlemg2kq  37618  cdlemg2m  37620  cdlemg7fvN  37640  cdlemg8a  37643  cdlemg11aq  37654  cdlemg10c  37655  cdlemg17a  37677  cdlemg31b0N  37710  cdlemg41  37734  cdlemh2  37832  cdlemi  37836  cdlemk21-2N  37907  dihmeetlem1N  38306  dihmeetlem13N  38335  iunrelexpmin1  39931
  Copyright terms: Public domain W3C validator