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  8372  omeu  8576  wemaplem3  9524  gruina  10831  expmordi  14235  4sqlem18  17060  vdwlem10  17088  mdetuni0  22849  mdetmul  22851  tsmsxp  24387  ax5seglem3  29396  btwnconn1lem1  36675  btwnconn1lem2  36676  btwnconn1lem3  36677  btwnconn1lem4  36678  btwnconn1lem12  36686  btwnconn1lem13  36687  linethru  36741  2llnjN  40448  2lplnja  40500  2lplnj  40501  cdlemblem  40674  dalaw  40767  pclfinN  40781  lhpmcvr4N  40907  lhp2atne  40915  lhp2at0ne  40917  cdlemb2  40922  cdlemd7  41085  cdleme01N  41102  cdleme02N  41103  cdleme0ex2N  41105  cdleme7aa  41123  cdleme7c  41126  cdleme7d  41127  cdleme7e  41128  cdleme7ga  41129  cdleme11a  41141  cdleme20k  41200  cdleme21d  41211  cdleme27cl  41247  cdlemefrs29bpre0  41277  cdlemefrs29cpre1  41279  cdlemefrs32fva  41281  cdlemefrs32fva1  41282  cdlemefr29exN  41283  cdlemefr32sn2aw  41285  cdlemefr31fv1  41292  cdlemefs32sn1aw  41295  cdlemefr44  41306  cdlemefr45e  41309  cdleme41sn3a  41314  cdleme35a  41329  cdleme35fnpq  41330  cdleme35b  41331  cdleme35c  41332  cdleme35d  41333  cdleme35e  41334  cdleme35f  41335  cdleme35sn3a  41340  cdleme42e  41360  cdleme42h  41363  cdleme42i  41364  cdleme17d2  41376  cdleme48fv  41380  cdleme48bw  41383  cdleme48b  41384  cdlemeg46c  41394  cdlemeg46ngfr  41399  cdleme48d  41416  cdlemg2kq  41483  cdlemg2m  41485  cdlemg7fvN  41505  cdlemg8a  41508  cdlemg11aq  41519  cdlemg10c  41520  cdlemg17a  41542  cdlemg31b0N  41575  cdlemg41  41599  cdlemh2  41697  cdlemi  41701  cdlemk21-2N  41772  dihmeetlem1N  42171  dihmeetlem13N  42200  iunrelexpmin1  44556