Theorem simp2rl 1259

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 1150	1 ⊢ ((𝜃 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏) → 𝜑)

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

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 1103

This theorem is referenced by:  tfrlem5  8354  omeu  8558  wemaplem3  9498  gruina  10791  expmordi  14194  4sqlem18  17012  vdwlem10  17040  mdetuni0  22739  mdetmul  22741  tsmsxp  24273  ax5seglem3  29190  btwnconn1lem1  36450  btwnconn1lem2  36451  btwnconn1lem3  36452  btwnconn1lem4  36453  btwnconn1lem12  36461  btwnconn1lem13  36462  linethru  36516  2llnjN  40203  2lplnja  40255  2lplnj  40256  cdlemblem  40429  dalaw  40522  pclfinN  40536  lhpmcvr4N  40662  lhp2atne  40670  lhp2at0ne  40672  cdlemb2  40677  cdlemd7  40840  cdleme01N  40857  cdleme02N  40858  cdleme0ex2N  40860  cdleme7aa  40878  cdleme7c  40881  cdleme7d  40882  cdleme7e  40883  cdleme7ga  40884  cdleme11a  40896  cdleme20k  40955  cdleme21d  40966  cdleme27cl  41002  cdlemefrs29bpre0  41032  cdlemefrs29cpre1  41034  cdlemefrs32fva  41036  cdlemefrs32fva1  41037  cdlemefr29exN  41038  cdlemefr32sn2aw  41040  cdlemefr31fv1  41047  cdlemefs32sn1aw  41050  cdlemefr44  41061  cdlemefr45e  41064  cdleme41sn3a  41069  cdleme35a  41084  cdleme35fnpq  41085  cdleme35b  41086  cdleme35c  41087  cdleme35d  41088  cdleme35e  41089  cdleme35f  41090  cdleme35sn3a  41095  cdleme42e  41115  cdleme42h  41118  cdleme42i  41119  cdleme17d2  41131  cdleme48fv  41135  cdleme48bw  41138  cdleme48b  41139  cdlemeg46c  41149  cdlemeg46ngfr  41154  cdleme48d  41171  cdlemg2kq  41238  cdlemg2m  41240  cdlemg7fvN  41260  cdlemg8a  41263  cdlemg11aq  41274  cdlemg10c  41275  cdlemg17a  41297  cdlemg31b0N  41330  cdlemg41  41354  cdlemh2  41452  cdlemi  41456  cdlemk21-2N  41527  dihmeetlem1N  41926  dihmeetlem13N  41955  iunrelexpmin1  44296