Theorem simp2rl 1244

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

Assertion

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

Proof of Theorem simp2rl

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  tfrlem5  8312  omeu  8513  wemaplem3  9456  gruina  10732  expmordi  14120  4sqlem18  16924  vdwlem10  16952  mdetuni0  22596  mdetmul  22598  tsmsxp  24130  ax5seglem3  29014  btwnconn1lem1  36285  btwnconn1lem2  36286  btwnconn1lem3  36287  btwnconn1lem4  36288  btwnconn1lem12  36296  btwnconn1lem13  36297  linethru  36351  2llnjN  40027  2lplnja  40079  2lplnj  40080  cdlemblem  40253  dalaw  40346  pclfinN  40360  lhpmcvr4N  40486  lhp2atne  40494  lhp2at0ne  40496  cdlemb2  40501  cdlemd7  40664  cdleme01N  40681  cdleme02N  40682  cdleme0ex2N  40684  cdleme7aa  40702  cdleme7c  40705  cdleme7d  40706  cdleme7e  40707  cdleme7ga  40708  cdleme11a  40720  cdleme20k  40779  cdleme21d  40790  cdleme27cl  40826  cdlemefrs29bpre0  40856  cdlemefrs29cpre1  40858  cdlemefrs32fva  40860  cdlemefrs32fva1  40861  cdlemefr29exN  40862  cdlemefr32sn2aw  40864  cdlemefr31fv1  40871  cdlemefs32sn1aw  40874  cdlemefr44  40885  cdlemefr45e  40888  cdleme41sn3a  40893  cdleme35a  40908  cdleme35fnpq  40909  cdleme35b  40910  cdleme35c  40911  cdleme35d  40912  cdleme35e  40913  cdleme35f  40914  cdleme35sn3a  40919  cdleme42e  40939  cdleme42h  40942  cdleme42i  40943  cdleme17d2  40955  cdleme48fv  40959  cdleme48bw  40962  cdleme48b  40963  cdlemeg46c  40973  cdlemeg46ngfr  40978  cdleme48d  40995  cdlemg2kq  41062  cdlemg2m  41064  cdlemg7fvN  41084  cdlemg8a  41087  cdlemg11aq  41098  cdlemg10c  41099  cdlemg17a  41121  cdlemg31b0N  41154  cdlemg41  41178  cdlemh2  41276  cdlemi  41280  cdlemk21-2N  41351  dihmeetlem1N  41750  dihmeetlem13N  41779  iunrelexpmin1  44153