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 782	. 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓)) → 𝜑)
2	1	3ad2ant2 1152	1 ⊢ ((𝜃 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  tfrlem5  8367  omeu  8571  wemaplem3  9511  gruina  10804  expmordi  14205  4sqlem18  17023  vdwlem10  17051  mdetuni0  22759  mdetmul  22761  tsmsxp  24293  ax5seglem3  29259  btwnconn1lem1  36557  btwnconn1lem2  36558  btwnconn1lem3  36559  btwnconn1lem4  36560  btwnconn1lem12  36568  btwnconn1lem13  36569  linethru  36623  2llnjN  40319  2lplnja  40371  2lplnj  40372  cdlemblem  40545  dalaw  40638  pclfinN  40652  lhpmcvr4N  40778  lhp2atne  40786  lhp2at0ne  40788  cdlemb2  40793  cdlemd7  40956  cdleme01N  40973  cdleme02N  40974  cdleme0ex2N  40976  cdleme7aa  40994  cdleme7c  40997  cdleme7d  40998  cdleme7e  40999  cdleme7ga  41000  cdleme11a  41012  cdleme20k  41071  cdleme21d  41082  cdleme27cl  41118  cdlemefrs29bpre0  41148  cdlemefrs29cpre1  41150  cdlemefrs32fva  41152  cdlemefrs32fva1  41153  cdlemefr29exN  41154  cdlemefr32sn2aw  41156  cdlemefr31fv1  41163  cdlemefs32sn1aw  41166  cdlemefr44  41177  cdlemefr45e  41180  cdleme41sn3a  41185  cdleme35a  41200  cdleme35fnpq  41201  cdleme35b  41202  cdleme35c  41203  cdleme35d  41204  cdleme35e  41205  cdleme35f  41206  cdleme35sn3a  41211  cdleme42e  41231  cdleme42h  41234  cdleme42i  41235  cdleme17d2  41247  cdleme48fv  41251  cdleme48bw  41254  cdleme48b  41255  cdlemeg46c  41265  cdlemeg46ngfr  41270  cdleme48d  41287  cdlemg2kq  41354  cdlemg2m  41356  cdlemg7fvN  41376  cdlemg8a  41379  cdlemg11aq  41390  cdlemg10c  41391  cdlemg17a  41413  cdlemg31b0N  41446  cdlemg41  41470  cdlemh2  41568  cdlemi  41572  cdlemk21-2N  41643  dihmeetlem1N  42042  dihmeetlem13N  42071  iunrelexpmin1  44414