Theorem simp2rl 1242

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 1134	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  8436  omeu  8641  wemaplem3  9617  gruina  10887  expmordi  14217  4sqlem18  17009  vdwlem10  17037  mdetuni0  22648  mdetmul  22650  tsmsxp  24184  ax5seglem3  28964  btwnconn1lem1  36051  btwnconn1lem2  36052  btwnconn1lem3  36053  btwnconn1lem4  36054  btwnconn1lem12  36062  btwnconn1lem13  36063  linethru  36117  2llnjN  39524  2lplnja  39576  2lplnj  39577  cdlemblem  39750  dalaw  39843  pclfinN  39857  lhpmcvr4N  39983  lhp2atne  39991  lhp2at0ne  39993  cdlemb2  39998  cdlemd7  40161  cdleme01N  40178  cdleme02N  40179  cdleme0ex2N  40181  cdleme7aa  40199  cdleme7c  40202  cdleme7d  40203  cdleme7e  40204  cdleme7ga  40205  cdleme11a  40217  cdleme20k  40276  cdleme21d  40287  cdleme27cl  40323  cdlemefrs29bpre0  40353  cdlemefrs29cpre1  40355  cdlemefrs32fva  40357  cdlemefrs32fva1  40358  cdlemefr29exN  40359  cdlemefr32sn2aw  40361  cdlemefr31fv1  40368  cdlemefs32sn1aw  40371  cdlemefr44  40382  cdlemefr45e  40385  cdleme41sn3a  40390  cdleme35a  40405  cdleme35fnpq  40406  cdleme35b  40407  cdleme35c  40408  cdleme35d  40409  cdleme35e  40410  cdleme35f  40411  cdleme35sn3a  40416  cdleme42e  40436  cdleme42h  40439  cdleme42i  40440  cdleme17d2  40452  cdleme48fv  40456  cdleme48bw  40459  cdleme48b  40460  cdlemeg46c  40470  cdlemeg46ngfr  40475  cdleme48d  40492  cdlemg2kq  40559  cdlemg2m  40561  cdlemg7fvN  40581  cdlemg8a  40584  cdlemg11aq  40595  cdlemg10c  40596  cdlemg17a  40618  cdlemg31b0N  40651  cdlemg41  40675  cdlemh2  40773  cdlemi  40777  cdlemk21-2N  40848  dihmeetlem1N  41247  dihmeetlem13N  41276  iunrelexpmin1  43670