Theorem simp2rl 1243

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Assertion

Ref	Expression
simp2rl	⊢ ((𝜃 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏) → 𝜑)

Proof of Theorem simp2rl

Step	Hyp	Ref	Expression
1		simprl 770	. 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓)) → 𝜑)
2	1	3ad2ant2 1134	1 ⊢ ((𝜃 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  tfrlem5  8394  omeu  8597  wemaplem3  9562  gruina  10832  expmordi  14185  4sqlem18  16982  vdwlem10  17010  mdetuni0  22559  mdetmul  22561  tsmsxp  24093  ax5seglem3  28910  btwnconn1lem1  36105  btwnconn1lem2  36106  btwnconn1lem3  36107  btwnconn1lem4  36108  btwnconn1lem12  36116  btwnconn1lem13  36117  linethru  36171  2llnjN  39586  2lplnja  39638  2lplnj  39639  cdlemblem  39812  dalaw  39905  pclfinN  39919  lhpmcvr4N  40045  lhp2atne  40053  lhp2at0ne  40055  cdlemb2  40060  cdlemd7  40223  cdleme01N  40240  cdleme02N  40241  cdleme0ex2N  40243  cdleme7aa  40261  cdleme7c  40264  cdleme7d  40265  cdleme7e  40266  cdleme7ga  40267  cdleme11a  40279  cdleme20k  40338  cdleme21d  40349  cdleme27cl  40385  cdlemefrs29bpre0  40415  cdlemefrs29cpre1  40417  cdlemefrs32fva  40419  cdlemefrs32fva1  40420  cdlemefr29exN  40421  cdlemefr32sn2aw  40423  cdlemefr31fv1  40430  cdlemefs32sn1aw  40433  cdlemefr44  40444  cdlemefr45e  40447  cdleme41sn3a  40452  cdleme35a  40467  cdleme35fnpq  40468  cdleme35b  40469  cdleme35c  40470  cdleme35d  40471  cdleme35e  40472  cdleme35f  40473  cdleme35sn3a  40478  cdleme42e  40498  cdleme42h  40501  cdleme42i  40502  cdleme17d2  40514  cdleme48fv  40518  cdleme48bw  40521  cdleme48b  40522  cdlemeg46c  40532  cdlemeg46ngfr  40537  cdleme48d  40554  cdlemg2kq  40621  cdlemg2m  40623  cdlemg7fvN  40643  cdlemg8a  40646  cdlemg11aq  40657  cdlemg10c  40658  cdlemg17a  40680  cdlemg31b0N  40713  cdlemg41  40737  cdlemh2  40835  cdlemi  40839  cdlemk21-2N  40910  dihmeetlem1N  41309  dihmeetlem13N  41338  iunrelexpmin1  43732