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

This theorem is referenced by:  tfrlem5  8182  omeu  8378  wemaplem3  9237  gruina  10505  expmordi  13813  4sqlem18  16591  vdwlem10  16619  mdetuni0  21678  mdetmul  21680  tsmsxp  23214  ax5seglem3  27202  btwnconn1lem1  34316  btwnconn1lem2  34317  btwnconn1lem3  34318  btwnconn1lem4  34319  btwnconn1lem12  34327  btwnconn1lem13  34328  linethru  34382  2llnjN  37508  2lplnja  37560  2lplnj  37561  cdlemblem  37734  dalaw  37827  pclfinN  37841  lhpmcvr4N  37967  lhp2atne  37975  lhp2at0ne  37977  cdlemb2  37982  cdlemd7  38145  cdleme01N  38162  cdleme02N  38163  cdleme0ex2N  38165  cdleme7aa  38183  cdleme7c  38186  cdleme7d  38187  cdleme7e  38188  cdleme7ga  38189  cdleme11a  38201  cdleme20k  38260  cdleme21d  38271  cdleme27cl  38307  cdlemefrs29bpre0  38337  cdlemefrs29cpre1  38339  cdlemefrs32fva  38341  cdlemefrs32fva1  38342  cdlemefr29exN  38343  cdlemefr32sn2aw  38345  cdlemefr31fv1  38352  cdlemefs32sn1aw  38355  cdlemefr44  38366  cdlemefr45e  38369  cdleme41sn3a  38374  cdleme35a  38389  cdleme35fnpq  38390  cdleme35b  38391  cdleme35c  38392  cdleme35d  38393  cdleme35e  38394  cdleme35f  38395  cdleme35sn3a  38400  cdleme42e  38420  cdleme42h  38423  cdleme42i  38424  cdleme17d2  38436  cdleme48fv  38440  cdleme48bw  38443  cdleme48b  38444  cdlemeg46c  38454  cdlemeg46ngfr  38459  cdleme48d  38476  cdlemg2kq  38543  cdlemg2m  38545  cdlemg7fvN  38565  cdlemg8a  38568  cdlemg11aq  38579  cdlemg10c  38580  cdlemg17a  38602  cdlemg31b0N  38635  cdlemg41  38659  cdlemh2  38757  cdlemi  38761  cdlemk21-2N  38832  dihmeetlem1N  39231  dihmeetlem13N  39260  iunrelexpmin1  41205