Theorem simp2rl 1249

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

Assertion

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

Proof of Theorem simp2rl

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  tfrlem5  8316  omeu  8517  wemaplem3  9460  gruina  10739  expmordi  14127  4sqlem18  16931  vdwlem10  16959  mdetuni0  22611  mdetmul  22613  tsmsxp  24145  ax5seglem3  29025  btwnconn1lem1  36322  btwnconn1lem2  36323  btwnconn1lem3  36324  btwnconn1lem4  36325  btwnconn1lem12  36333  btwnconn1lem13  36334  linethru  36388  2llnjN  40066  2lplnja  40118  2lplnj  40119  cdlemblem  40292  dalaw  40385  pclfinN  40399  lhpmcvr4N  40525  lhp2atne  40533  lhp2at0ne  40535  cdlemb2  40540  cdlemd7  40703  cdleme01N  40720  cdleme02N  40721  cdleme0ex2N  40723  cdleme7aa  40741  cdleme7c  40744  cdleme7d  40745  cdleme7e  40746  cdleme7ga  40747  cdleme11a  40759  cdleme20k  40818  cdleme21d  40829  cdleme27cl  40865  cdlemefrs29bpre0  40895  cdlemefrs29cpre1  40897  cdlemefrs32fva  40899  cdlemefrs32fva1  40900  cdlemefr29exN  40901  cdlemefr32sn2aw  40903  cdlemefr31fv1  40910  cdlemefs32sn1aw  40913  cdlemefr44  40924  cdlemefr45e  40927  cdleme41sn3a  40932  cdleme35a  40947  cdleme35fnpq  40948  cdleme35b  40949  cdleme35c  40950  cdleme35d  40951  cdleme35e  40952  cdleme35f  40953  cdleme35sn3a  40958  cdleme42e  40978  cdleme42h  40981  cdleme42i  40982  cdleme17d2  40994  cdleme48fv  40998  cdleme48bw  41001  cdleme48b  41002  cdlemeg46c  41012  cdlemeg46ngfr  41017  cdleme48d  41034  cdlemg2kq  41101  cdlemg2m  41103  cdlemg7fvN  41123  cdlemg8a  41126  cdlemg11aq  41137  cdlemg10c  41138  cdlemg17a  41160  cdlemg31b0N  41193  cdlemg41  41217  cdlemh2  41315  cdlemi  41319  cdlemk21-2N  41390  dihmeetlem1N  41789  dihmeetlem13N  41818  iunrelexpmin1  44159