Theorem simp2rl 1261

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

Assertion

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

Proof of Theorem simp2rl

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  tfrlem5  8418  omeu  8624  wemaplem3  9572  gruina  10933  expmordi  14340  4sqlem18  17172  vdwlem10  17200  mdetuni0  22969  mdetmul  22971  tsmsxp  24507  ax5seglem3  29542  btwnconn1lem1  37043  btwnconn1lem2  37044  btwnconn1lem3  37045  btwnconn1lem4  37046  btwnconn1lem12  37054  btwnconn1lem13  37055  linethru  37109  2llnjN  40827  2lplnja  40879  2lplnj  40880  cdlemblem  41053  dalaw  41146  pclfinN  41160  lhpmcvr4N  41286  lhp2atne  41294  lhp2at0ne  41296  cdlemb2  41301  cdlemd7  41464  cdleme01N  41481  cdleme02N  41482  cdleme0ex2N  41484  cdleme7aa  41502  cdleme7c  41505  cdleme7d  41506  cdleme7e  41507  cdleme7ga  41508  cdleme11a  41520  cdleme20k  41579  cdleme21d  41590  cdleme27cl  41626  cdlemefrs29bpre0  41656  cdlemefrs29cpre1  41658  cdlemefrs32fva  41660  cdlemefrs32fva1  41661  cdlemefr29exN  41662  cdlemefr32sn2aw  41664  cdlemefr31fv1  41671  cdlemefs32sn1aw  41674  cdlemefr44  41685  cdlemefr45e  41688  cdleme41sn3a  41693  cdleme35a  41708  cdleme35fnpq  41709  cdleme35b  41710  cdleme35c  41711  cdleme35d  41712  cdleme35e  41713  cdleme35f  41714  cdleme35sn3a  41719  cdleme42e  41739  cdleme42h  41742  cdleme42i  41743  cdleme17d2  41755  cdleme48fv  41759  cdleme48bw  41762  cdleme48b  41763  cdlemeg46c  41773  cdlemeg46ngfr  41778  cdleme48d  41795  cdlemg2kq  41862  cdlemg2m  41864  cdlemg7fvN  41884  cdlemg8a  41887  cdlemg11aq  41898  cdlemg10c  41899  cdlemg17a  41921  cdlemg31b0N  41954  cdlemg41  41978  cdlemh2  42076  cdlemi  42080  cdlemk21-2N  42151  dihmeetlem1N  42550  dihmeetlem13N  42579  iunrelexpmin1  44911