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  8387  omeu  8593  wemaplem3  9542  gruina  10903  expmordi  14310  4sqlem18  17140  vdwlem10  17168  mdetuni0  22936  mdetmul  22938  tsmsxp  24474  ax5seglem3  29509  btwnconn1lem1  36852  btwnconn1lem2  36853  btwnconn1lem3  36854  btwnconn1lem4  36855  btwnconn1lem12  36863  btwnconn1lem13  36864  linethru  36918  2llnjN  40625  2lplnja  40677  2lplnj  40678  cdlemblem  40851  dalaw  40944  pclfinN  40958  lhpmcvr4N  41084  lhp2atne  41092  lhp2at0ne  41094  cdlemb2  41099  cdlemd7  41262  cdleme01N  41279  cdleme02N  41280  cdleme0ex2N  41282  cdleme7aa  41300  cdleme7c  41303  cdleme7d  41304  cdleme7e  41305  cdleme7ga  41306  cdleme11a  41318  cdleme20k  41377  cdleme21d  41388  cdleme27cl  41424  cdlemefrs29bpre0  41454  cdlemefrs29cpre1  41456  cdlemefrs32fva  41458  cdlemefrs32fva1  41459  cdlemefr29exN  41460  cdlemefr32sn2aw  41462  cdlemefr31fv1  41469  cdlemefs32sn1aw  41472  cdlemefr44  41483  cdlemefr45e  41486  cdleme41sn3a  41491  cdleme35a  41506  cdleme35fnpq  41507  cdleme35b  41508  cdleme35c  41509  cdleme35d  41510  cdleme35e  41511  cdleme35f  41512  cdleme35sn3a  41517  cdleme42e  41537  cdleme42h  41540  cdleme42i  41541  cdleme17d2  41553  cdleme48fv  41557  cdleme48bw  41560  cdleme48b  41561  cdlemeg46c  41571  cdlemeg46ngfr  41576  cdleme48d  41593  cdlemg2kq  41660  cdlemg2m  41662  cdlemg7fvN  41682  cdlemg8a  41685  cdlemg11aq  41696  cdlemg10c  41697  cdlemg17a  41719  cdlemg31b0N  41752  cdlemg41  41776  cdlemh2  41874  cdlemi  41878  cdlemk21-2N  41949  dihmeetlem1N  42348  dihmeetlem13N  42377  iunrelexpmin1  44708