Theorem simp2rl 1242

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

Assertion

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

Proof of Theorem simp2rl

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1087

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 397  df-3an 1089

This theorem is referenced by:  tfrlem5  8379  omeu  8584  wemaplem3  9542  gruina  10812  expmordi  14131  4sqlem18  16894  vdwlem10  16922  mdetuni0  22122  mdetmul  22124  tsmsxp  23658  ax5seglem3  28186  btwnconn1lem1  35054  btwnconn1lem2  35055  btwnconn1lem3  35056  btwnconn1lem4  35057  btwnconn1lem12  35065  btwnconn1lem13  35066  linethru  35120  2llnjN  38433  2lplnja  38485  2lplnj  38486  cdlemblem  38659  dalaw  38752  pclfinN  38766  lhpmcvr4N  38892  lhp2atne  38900  lhp2at0ne  38902  cdlemb2  38907  cdlemd7  39070  cdleme01N  39087  cdleme02N  39088  cdleme0ex2N  39090  cdleme7aa  39108  cdleme7c  39111  cdleme7d  39112  cdleme7e  39113  cdleme7ga  39114  cdleme11a  39126  cdleme20k  39185  cdleme21d  39196  cdleme27cl  39232  cdlemefrs29bpre0  39262  cdlemefrs29cpre1  39264  cdlemefrs32fva  39266  cdlemefrs32fva1  39267  cdlemefr29exN  39268  cdlemefr32sn2aw  39270  cdlemefr31fv1  39277  cdlemefs32sn1aw  39280  cdlemefr44  39291  cdlemefr45e  39294  cdleme41sn3a  39299  cdleme35a  39314  cdleme35fnpq  39315  cdleme35b  39316  cdleme35c  39317  cdleme35d  39318  cdleme35e  39319  cdleme35f  39320  cdleme35sn3a  39325  cdleme42e  39345  cdleme42h  39348  cdleme42i  39349  cdleme17d2  39361  cdleme48fv  39365  cdleme48bw  39368  cdleme48b  39369  cdlemeg46c  39379  cdlemeg46ngfr  39384  cdleme48d  39401  cdlemg2kq  39468  cdlemg2m  39470  cdlemg7fvN  39490  cdlemg8a  39493  cdlemg11aq  39504  cdlemg10c  39505  cdlemg17a  39527  cdlemg31b0N  39560  cdlemg41  39584  cdlemh2  39682  cdlemi  39686  cdlemk21-2N  39757  dihmeetlem1N  40156  dihmeetlem13N  40185  iunrelexpmin1  42449