Theorem simp2rl 1243

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

Assertion

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

Proof of Theorem simp2rl

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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 398  df-3an 1090

This theorem is referenced by:  tfrlem5  8380  omeu  8585  wemaplem3  9543  gruina  10813  expmordi  14132  4sqlem18  16895  vdwlem10  16923  mdetuni0  22123  mdetmul  22125  tsmsxp  23659  ax5seglem3  28189  btwnconn1lem1  35059  btwnconn1lem2  35060  btwnconn1lem3  35061  btwnconn1lem4  35062  btwnconn1lem12  35070  btwnconn1lem13  35071  linethru  35125  2llnjN  38438  2lplnja  38490  2lplnj  38491  cdlemblem  38664  dalaw  38757  pclfinN  38771  lhpmcvr4N  38897  lhp2atne  38905  lhp2at0ne  38907  cdlemb2  38912  cdlemd7  39075  cdleme01N  39092  cdleme02N  39093  cdleme0ex2N  39095  cdleme7aa  39113  cdleme7c  39116  cdleme7d  39117  cdleme7e  39118  cdleme7ga  39119  cdleme11a  39131  cdleme20k  39190  cdleme21d  39201  cdleme27cl  39237  cdlemefrs29bpre0  39267  cdlemefrs29cpre1  39269  cdlemefrs32fva  39271  cdlemefrs32fva1  39272  cdlemefr29exN  39273  cdlemefr32sn2aw  39275  cdlemefr31fv1  39282  cdlemefs32sn1aw  39285  cdlemefr44  39296  cdlemefr45e  39299  cdleme41sn3a  39304  cdleme35a  39319  cdleme35fnpq  39320  cdleme35b  39321  cdleme35c  39322  cdleme35d  39323  cdleme35e  39324  cdleme35f  39325  cdleme35sn3a  39330  cdleme42e  39350  cdleme42h  39353  cdleme42i  39354  cdleme17d2  39366  cdleme48fv  39370  cdleme48bw  39373  cdleme48b  39374  cdlemeg46c  39384  cdlemeg46ngfr  39389  cdleme48d  39406  cdlemg2kq  39473  cdlemg2m  39475  cdlemg7fvN  39495  cdlemg8a  39498  cdlemg11aq  39509  cdlemg10c  39510  cdlemg17a  39532  cdlemg31b0N  39565  cdlemg41  39589  cdlemh2  39687  cdlemi  39691  cdlemk21-2N  39762  dihmeetlem1N  40161  dihmeetlem13N  40190  iunrelexpmin1  42459