Theorem simp2rl 1239

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 1131	1 ⊢ ((𝜃 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  tfrlem5  8026  omeu  8221  wemaplem3  9045  gruina  10278  expmordi  13581  4sqlem18  16353  vdwlem10  16381  mdetuni0  21321  mdetmul  21323  tsmsxp  22855  ax5seglem3  26824  btwnconn1lem1  33938  btwnconn1lem2  33939  btwnconn1lem3  33940  btwnconn1lem4  33941  btwnconn1lem12  33949  btwnconn1lem13  33950  linethru  34004  2llnjN  37143  2lplnja  37195  2lplnj  37196  cdlemblem  37369  dalaw  37462  pclfinN  37476  lhpmcvr4N  37602  lhp2atne  37610  lhp2at0ne  37612  cdlemb2  37617  cdlemd7  37780  cdleme01N  37797  cdleme02N  37798  cdleme0ex2N  37800  cdleme7aa  37818  cdleme7c  37821  cdleme7d  37822  cdleme7e  37823  cdleme7ga  37824  cdleme11a  37836  cdleme20k  37895  cdleme21d  37906  cdleme27cl  37942  cdlemefrs29bpre0  37972  cdlemefrs29cpre1  37974  cdlemefrs32fva  37976  cdlemefrs32fva1  37977  cdlemefr29exN  37978  cdlemefr32sn2aw  37980  cdlemefr31fv1  37987  cdlemefs32sn1aw  37990  cdlemefr44  38001  cdlemefr45e  38004  cdleme41sn3a  38009  cdleme35a  38024  cdleme35fnpq  38025  cdleme35b  38026  cdleme35c  38027  cdleme35d  38028  cdleme35e  38029  cdleme35f  38030  cdleme35sn3a  38035  cdleme42e  38055  cdleme42h  38058  cdleme42i  38059  cdleme17d2  38071  cdleme48fv  38075  cdleme48bw  38078  cdleme48b  38079  cdlemeg46c  38089  cdlemeg46ngfr  38094  cdleme48d  38111  cdlemg2kq  38178  cdlemg2m  38180  cdlemg7fvN  38200  cdlemg8a  38203  cdlemg11aq  38214  cdlemg10c  38215  cdlemg17a  38237  cdlemg31b0N  38270  cdlemg41  38294  cdlemh2  38392  cdlemi  38396  cdlemk21-2N  38467  dihmeetlem1N  38866  dihmeetlem13N  38895  iunrelexpmin1  40782