Theorem simp2rl 1261

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

Assertion

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

Proof of Theorem simp2rl

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  tfrlem5  8371  omeu  8577  wemaplem3  9526  gruina  10884  expmordi  14290  4sqlem18  17120  vdwlem10  17148  mdetuni0  22916  mdetmul  22918  tsmsxp  24454  ax5seglem3  29491  btwnconn1lem1  36822  btwnconn1lem2  36823  btwnconn1lem3  36824  btwnconn1lem4  36825  btwnconn1lem12  36833  btwnconn1lem13  36834  linethru  36888  2llnjN  40592  2lplnja  40644  2lplnj  40645  cdlemblem  40818  dalaw  40911  pclfinN  40925  lhpmcvr4N  41051  lhp2atne  41059  lhp2at0ne  41061  cdlemb2  41066  cdlemd7  41229  cdleme01N  41246  cdleme02N  41247  cdleme0ex2N  41249  cdleme7aa  41267  cdleme7c  41270  cdleme7d  41271  cdleme7e  41272  cdleme7ga  41273  cdleme11a  41285  cdleme20k  41344  cdleme21d  41355  cdleme27cl  41391  cdlemefrs29bpre0  41421  cdlemefrs29cpre1  41423  cdlemefrs32fva  41425  cdlemefrs32fva1  41426  cdlemefr29exN  41427  cdlemefr32sn2aw  41429  cdlemefr31fv1  41436  cdlemefs32sn1aw  41439  cdlemefr44  41450  cdlemefr45e  41453  cdleme41sn3a  41458  cdleme35a  41473  cdleme35fnpq  41474  cdleme35b  41475  cdleme35c  41476  cdleme35d  41477  cdleme35e  41478  cdleme35f  41479  cdleme35sn3a  41484  cdleme42e  41504  cdleme42h  41507  cdleme42i  41508  cdleme17d2  41520  cdleme48fv  41524  cdleme48bw  41527  cdleme48b  41528  cdlemeg46c  41538  cdlemeg46ngfr  41543  cdleme48d  41560  cdlemg2kq  41627  cdlemg2m  41629  cdlemg7fvN  41649  cdlemg8a  41652  cdlemg11aq  41663  cdlemg10c  41664  cdlemg17a  41686  cdlemg31b0N  41719  cdlemg41  41743  cdlemh2  41841  cdlemi  41845  cdlemk21-2N  41916  dihmeetlem1N  42315  dihmeetlem13N  42344  iunrelexpmin1  44667