Theorem simp2rl 1239

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

Assertion

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

Proof of Theorem simp2rl

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

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

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 206  df-an 396  df-3an 1086

This theorem is referenced by:  tfrlem5  8376  omeu  8581  wemaplem3  9540  gruina  10810  expmordi  14130  4sqlem18  16896  vdwlem10  16924  mdetuni0  22447  mdetmul  22449  tsmsxp  23983  ax5seglem3  28661  btwnconn1lem1  35555  btwnconn1lem2  35556  btwnconn1lem3  35557  btwnconn1lem4  35558  btwnconn1lem12  35566  btwnconn1lem13  35567  linethru  35621  2llnjN  38932  2lplnja  38984  2lplnj  38985  cdlemblem  39158  dalaw  39251  pclfinN  39265  lhpmcvr4N  39391  lhp2atne  39399  lhp2at0ne  39401  cdlemb2  39406  cdlemd7  39569  cdleme01N  39586  cdleme02N  39587  cdleme0ex2N  39589  cdleme7aa  39607  cdleme7c  39610  cdleme7d  39611  cdleme7e  39612  cdleme7ga  39613  cdleme11a  39625  cdleme20k  39684  cdleme21d  39695  cdleme27cl  39731  cdlemefrs29bpre0  39761  cdlemefrs29cpre1  39763  cdlemefrs32fva  39765  cdlemefrs32fva1  39766  cdlemefr29exN  39767  cdlemefr32sn2aw  39769  cdlemefr31fv1  39776  cdlemefs32sn1aw  39779  cdlemefr44  39790  cdlemefr45e  39793  cdleme41sn3a  39798  cdleme35a  39813  cdleme35fnpq  39814  cdleme35b  39815  cdleme35c  39816  cdleme35d  39817  cdleme35e  39818  cdleme35f  39819  cdleme35sn3a  39824  cdleme42e  39844  cdleme42h  39847  cdleme42i  39848  cdleme17d2  39860  cdleme48fv  39864  cdleme48bw  39867  cdleme48b  39868  cdlemeg46c  39878  cdlemeg46ngfr  39883  cdleme48d  39900  cdlemg2kq  39967  cdlemg2m  39969  cdlemg7fvN  39989  cdlemg8a  39992  cdlemg11aq  40003  cdlemg10c  40004  cdlemg17a  40026  cdlemg31b0N  40059  cdlemg41  40083  cdlemh2  40181  cdlemi  40185  cdlemk21-2N  40256  dihmeetlem1N  40655  dihmeetlem13N  40684  iunrelexpmin1  42973