Theorem simp2rl 1244

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

Assertion

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

Proof of Theorem simp2rl

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1089

This theorem is referenced by:  tfrlem5  8319  omeu  8520  wemaplem3  9463  gruina  10741  expmordi  14129  4sqlem18  16933  vdwlem10  16961  mdetuni0  22586  mdetmul  22588  tsmsxp  24120  ax5seglem3  29000  btwnconn1lem1  36269  btwnconn1lem2  36270  btwnconn1lem3  36271  btwnconn1lem4  36272  btwnconn1lem12  36280  btwnconn1lem13  36281  linethru  36335  2llnjN  40013  2lplnja  40065  2lplnj  40066  cdlemblem  40239  dalaw  40332  pclfinN  40346  lhpmcvr4N  40472  lhp2atne  40480  lhp2at0ne  40482  cdlemb2  40487  cdlemd7  40650  cdleme01N  40667  cdleme02N  40668  cdleme0ex2N  40670  cdleme7aa  40688  cdleme7c  40691  cdleme7d  40692  cdleme7e  40693  cdleme7ga  40694  cdleme11a  40706  cdleme20k  40765  cdleme21d  40776  cdleme27cl  40812  cdlemefrs29bpre0  40842  cdlemefrs29cpre1  40844  cdlemefrs32fva  40846  cdlemefrs32fva1  40847  cdlemefr29exN  40848  cdlemefr32sn2aw  40850  cdlemefr31fv1  40857  cdlemefs32sn1aw  40860  cdlemefr44  40871  cdlemefr45e  40874  cdleme41sn3a  40879  cdleme35a  40894  cdleme35fnpq  40895  cdleme35b  40896  cdleme35c  40897  cdleme35d  40898  cdleme35e  40899  cdleme35f  40900  cdleme35sn3a  40905  cdleme42e  40925  cdleme42h  40928  cdleme42i  40929  cdleme17d2  40941  cdleme48fv  40945  cdleme48bw  40948  cdleme48b  40949  cdlemeg46c  40959  cdlemeg46ngfr  40964  cdleme48d  40981  cdlemg2kq  41048  cdlemg2m  41050  cdlemg7fvN  41070  cdlemg8a  41073  cdlemg11aq  41084  cdlemg10c  41085  cdlemg17a  41107  cdlemg31b0N  41140  cdlemg41  41164  cdlemh2  41262  cdlemi  41266  cdlemk21-2N  41337  dihmeetlem1N  41736  dihmeetlem13N  41765  iunrelexpmin1  44135