Theorem simp2rl 1240

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

Assertion

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

Proof of Theorem simp2rl

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

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1085

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 395  df-3an 1087

This theorem is referenced by:  tfrlem5  8382  omeu  8587  wemaplem3  9545  gruina  10815  expmordi  14136  4sqlem18  16899  vdwlem10  16927  mdetuni0  22343  mdetmul  22345  tsmsxp  23879  ax5seglem3  28456  btwnconn1lem1  35363  btwnconn1lem2  35364  btwnconn1lem3  35365  btwnconn1lem4  35366  btwnconn1lem12  35374  btwnconn1lem13  35375  linethru  35429  2llnjN  38741  2lplnja  38793  2lplnj  38794  cdlemblem  38967  dalaw  39060  pclfinN  39074  lhpmcvr4N  39200  lhp2atne  39208  lhp2at0ne  39210  cdlemb2  39215  cdlemd7  39378  cdleme01N  39395  cdleme02N  39396  cdleme0ex2N  39398  cdleme7aa  39416  cdleme7c  39419  cdleme7d  39420  cdleme7e  39421  cdleme7ga  39422  cdleme11a  39434  cdleme20k  39493  cdleme21d  39504  cdleme27cl  39540  cdlemefrs29bpre0  39570  cdlemefrs29cpre1  39572  cdlemefrs32fva  39574  cdlemefrs32fva1  39575  cdlemefr29exN  39576  cdlemefr32sn2aw  39578  cdlemefr31fv1  39585  cdlemefs32sn1aw  39588  cdlemefr44  39599  cdlemefr45e  39602  cdleme41sn3a  39607  cdleme35a  39622  cdleme35fnpq  39623  cdleme35b  39624  cdleme35c  39625  cdleme35d  39626  cdleme35e  39627  cdleme35f  39628  cdleme35sn3a  39633  cdleme42e  39653  cdleme42h  39656  cdleme42i  39657  cdleme17d2  39669  cdleme48fv  39673  cdleme48bw  39676  cdleme48b  39677  cdlemeg46c  39687  cdlemeg46ngfr  39692  cdleme48d  39709  cdlemg2kq  39776  cdlemg2m  39778  cdlemg7fvN  39798  cdlemg8a  39801  cdlemg11aq  39812  cdlemg10c  39813  cdlemg17a  39835  cdlemg31b0N  39868  cdlemg41  39892  cdlemh2  39990  cdlemi  39994  cdlemk21-2N  40065  dihmeetlem1N  40464  dihmeetlem13N  40493  iunrelexpmin1  42761