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  8390  omeu  8596  wemaplem3  9545  gruina  10906  expmordi  14313  4sqlem18  17145  vdwlem10  17173  mdetuni0  22941  mdetmul  22943  tsmsxp  24479  ax5seglem3  29514  btwnconn1lem1  36944  btwnconn1lem2  36945  btwnconn1lem3  36946  btwnconn1lem4  36947  btwnconn1lem12  36955  btwnconn1lem13  36956  linethru  37010  2llnjN  40717  2lplnja  40769  2lplnj  40770  cdlemblem  40943  dalaw  41036  pclfinN  41050  lhpmcvr4N  41176  lhp2atne  41184  lhp2at0ne  41186  cdlemb2  41191  cdlemd7  41354  cdleme01N  41371  cdleme02N  41372  cdleme0ex2N  41374  cdleme7aa  41392  cdleme7c  41395  cdleme7d  41396  cdleme7e  41397  cdleme7ga  41398  cdleme11a  41410  cdleme20k  41469  cdleme21d  41480  cdleme27cl  41516  cdlemefrs29bpre0  41546  cdlemefrs29cpre1  41548  cdlemefrs32fva  41550  cdlemefrs32fva1  41551  cdlemefr29exN  41552  cdlemefr32sn2aw  41554  cdlemefr31fv1  41561  cdlemefs32sn1aw  41564  cdlemefr44  41575  cdlemefr45e  41578  cdleme41sn3a  41583  cdleme35a  41598  cdleme35fnpq  41599  cdleme35b  41600  cdleme35c  41601  cdleme35d  41602  cdleme35e  41603  cdleme35f  41604  cdleme35sn3a  41609  cdleme42e  41629  cdleme42h  41632  cdleme42i  41633  cdleme17d2  41645  cdleme48fv  41649  cdleme48bw  41652  cdleme48b  41653  cdlemeg46c  41663  cdlemeg46ngfr  41668  cdleme48d  41685  cdlemg2kq  41752  cdlemg2m  41754  cdlemg7fvN  41774  cdlemg8a  41777  cdlemg11aq  41788  cdlemg10c  41789  cdlemg17a  41811  cdlemg31b0N  41844  cdlemg41  41868  cdlemh2  41966  cdlemi  41970  cdlemk21-2N  42041  dihmeetlem1N  42440  dihmeetlem13N  42469  iunrelexpmin1  44801