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  7436  omeu  7625  wemaplem3  8413  gruina  9600  4sqlem18  15609  vdwlem10  15637  mdetuni0  20367  mdetmul  20369  tsmsxp  21898  ax5seglem3  25745  btwnconn1lem1  31889  btwnconn1lem2  31890  btwnconn1lem3  31891  btwnconn1lem4  31892  btwnconn1lem12  31900  btwnconn1lem13  31901  linethru  31955  2llnjN  34372  2lplnja  34424  2lplnj  34425  cdlemblem  34598  dalaw  34691  pclfinN  34705  lhpmcvr4N  34831  lhp2atne  34839  lhp2at0ne  34841  cdlemb2  34846  cdlemd7  35010  cdleme01N  35027  cdleme02N  35028  cdleme0ex2N  35030  cdleme7aa  35048  cdleme7c  35051  cdleme7d  35052  cdleme7e  35053  cdleme7ga  35054  cdleme11a  35066  cdleme20k  35126  cdleme21d  35137  cdleme27cl  35173  cdlemefrs29bpre0  35203  cdlemefrs29cpre1  35205  cdlemefrs32fva  35207  cdlemefrs32fva1  35208  cdlemefr29exN  35209  cdlemefr32sn2aw  35211  cdlemefr31fv1  35218  cdlemefs32sn1aw  35221  cdlemefr44  35232  cdlemefr45e  35235  cdleme41sn3a  35240  cdleme35a  35255  cdleme35fnpq  35256  cdleme35b  35257  cdleme35c  35258  cdleme35d  35259  cdleme35e  35260  cdleme35f  35261  cdleme35sn3a  35266  cdleme42e  35286  cdleme42h  35289  cdleme42i  35290  cdleme17d2  35302  cdleme48fv  35306  cdleme48bw  35309  cdleme48b  35310  cdlemeg46c  35320  cdlemeg46ngfr  35325  cdleme48d  35342  cdlemg2kq  35409  cdlemg2m  35411  cdlemg7fvN  35431  cdlemg8a  35434  cdlemg11aq  35445  cdlemg10c  35446  cdlemg17a  35468  cdlemg31b0N  35501  cdlemg41  35525  cdlemh2  35623  cdlemi  35627  cdlemk21-2N  35698  dihmeetlem1N  36098  dihmeetlem13N  36127  expmordi  37031  iunrelexpmin1  37520
  Copyright terms: Public domain W3C validator