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  8351  omeu  8552  wemaplem3  9508  gruina  10778  expmordi  14139  4sqlem18  16940  vdwlem10  16968  mdetuni0  22515  mdetmul  22517  tsmsxp  24049  ax5seglem3  28865  btwnconn1lem1  36082  btwnconn1lem2  36083  btwnconn1lem3  36084  btwnconn1lem4  36085  btwnconn1lem12  36093  btwnconn1lem13  36094  linethru  36148  2llnjN  39568  2lplnja  39620  2lplnj  39621  cdlemblem  39794  dalaw  39887  pclfinN  39901  lhpmcvr4N  40027  lhp2atne  40035  lhp2at0ne  40037  cdlemb2  40042  cdlemd7  40205  cdleme01N  40222  cdleme02N  40223  cdleme0ex2N  40225  cdleme7aa  40243  cdleme7c  40246  cdleme7d  40247  cdleme7e  40248  cdleme7ga  40249  cdleme11a  40261  cdleme20k  40320  cdleme21d  40331  cdleme27cl  40367  cdlemefrs29bpre0  40397  cdlemefrs29cpre1  40399  cdlemefrs32fva  40401  cdlemefrs32fva1  40402  cdlemefr29exN  40403  cdlemefr32sn2aw  40405  cdlemefr31fv1  40412  cdlemefs32sn1aw  40415  cdlemefr44  40426  cdlemefr45e  40429  cdleme41sn3a  40434  cdleme35a  40449  cdleme35fnpq  40450  cdleme35b  40451  cdleme35c  40452  cdleme35d  40453  cdleme35e  40454  cdleme35f  40455  cdleme35sn3a  40460  cdleme42e  40480  cdleme42h  40483  cdleme42i  40484  cdleme17d2  40496  cdleme48fv  40500  cdleme48bw  40503  cdleme48b  40504  cdlemeg46c  40514  cdlemeg46ngfr  40519  cdleme48d  40536  cdlemg2kq  40603  cdlemg2m  40605  cdlemg7fvN  40625  cdlemg8a  40628  cdlemg11aq  40639  cdlemg10c  40640  cdlemg17a  40662  cdlemg31b0N  40695  cdlemg41  40719  cdlemh2  40817  cdlemi  40821  cdlemk21-2N  40892  dihmeetlem1N  41291  dihmeetlem13N  41320  iunrelexpmin1  43704