Theorem simp2rl 1255

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

Assertion

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

Proof of Theorem simp2rl

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

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

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  tfrlem5  8345  omeu  8549  wemaplem3  9493  gruina  10773  expmordi  14177  4sqlem18  16981  vdwlem10  17009  mdetuni0  22661  mdetmul  22663  tsmsxp  24195  ax5seglem3  29078  btwnconn1lem1  36401  btwnconn1lem2  36402  btwnconn1lem3  36403  btwnconn1lem4  36404  btwnconn1lem12  36412  btwnconn1lem13  36413  linethru  36467  2llnjN  40155  2lplnja  40207  2lplnj  40208  cdlemblem  40381  dalaw  40474  pclfinN  40488  lhpmcvr4N  40614  lhp2atne  40622  lhp2at0ne  40624  cdlemb2  40629  cdlemd7  40792  cdleme01N  40809  cdleme02N  40810  cdleme0ex2N  40812  cdleme7aa  40830  cdleme7c  40833  cdleme7d  40834  cdleme7e  40835  cdleme7ga  40836  cdleme11a  40848  cdleme20k  40907  cdleme21d  40918  cdleme27cl  40954  cdlemefrs29bpre0  40984  cdlemefrs29cpre1  40986  cdlemefrs32fva  40988  cdlemefrs32fva1  40989  cdlemefr29exN  40990  cdlemefr32sn2aw  40992  cdlemefr31fv1  40999  cdlemefs32sn1aw  41002  cdlemefr44  41013  cdlemefr45e  41016  cdleme41sn3a  41021  cdleme35a  41036  cdleme35fnpq  41037  cdleme35b  41038  cdleme35c  41039  cdleme35d  41040  cdleme35e  41041  cdleme35f  41042  cdleme35sn3a  41047  cdleme42e  41067  cdleme42h  41070  cdleme42i  41071  cdleme17d2  41083  cdleme48fv  41087  cdleme48bw  41090  cdleme48b  41091  cdlemeg46c  41101  cdlemeg46ngfr  41106  cdleme48d  41123  cdlemg2kq  41190  cdlemg2m  41192  cdlemg7fvN  41212  cdlemg8a  41215  cdlemg11aq  41226  cdlemg10c  41227  cdlemg17a  41249  cdlemg31b0N  41282  cdlemg41  41306  cdlemh2  41404  cdlemi  41408  cdlemk21-2N  41479  dihmeetlem1N  41878  dihmeetlem13N  41907  iunrelexpmin1  44248