Theorem simp2rl 1241

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 1133	1 ⊢ ((𝜃 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1086

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 397  df-3an 1088

This theorem is referenced by:  tfrlem5  8220  omeu  8425  wemaplem3  9316  gruina  10583  expmordi  13894  4sqlem18  16672  vdwlem10  16700  mdetuni0  21779  mdetmul  21781  tsmsxp  23315  ax5seglem3  27308  btwnconn1lem1  34398  btwnconn1lem2  34399  btwnconn1lem3  34400  btwnconn1lem4  34401  btwnconn1lem12  34409  btwnconn1lem13  34410  linethru  34464  2llnjN  37588  2lplnja  37640  2lplnj  37641  cdlemblem  37814  dalaw  37907  pclfinN  37921  lhpmcvr4N  38047  lhp2atne  38055  lhp2at0ne  38057  cdlemb2  38062  cdlemd7  38225  cdleme01N  38242  cdleme02N  38243  cdleme0ex2N  38245  cdleme7aa  38263  cdleme7c  38266  cdleme7d  38267  cdleme7e  38268  cdleme7ga  38269  cdleme11a  38281  cdleme20k  38340  cdleme21d  38351  cdleme27cl  38387  cdlemefrs29bpre0  38417  cdlemefrs29cpre1  38419  cdlemefrs32fva  38421  cdlemefrs32fva1  38422  cdlemefr29exN  38423  cdlemefr32sn2aw  38425  cdlemefr31fv1  38432  cdlemefs32sn1aw  38435  cdlemefr44  38446  cdlemefr45e  38449  cdleme41sn3a  38454  cdleme35a  38469  cdleme35fnpq  38470  cdleme35b  38471  cdleme35c  38472  cdleme35d  38473  cdleme35e  38474  cdleme35f  38475  cdleme35sn3a  38480  cdleme42e  38500  cdleme42h  38503  cdleme42i  38504  cdleme17d2  38516  cdleme48fv  38520  cdleme48bw  38523  cdleme48b  38524  cdlemeg46c  38534  cdlemeg46ngfr  38539  cdleme48d  38556  cdlemg2kq  38623  cdlemg2m  38625  cdlemg7fvN  38645  cdlemg8a  38648  cdlemg11aq  38659  cdlemg10c  38660  cdlemg17a  38682  cdlemg31b0N  38715  cdlemg41  38739  cdlemh2  38837  cdlemi  38841  cdlemk21-2N  38912  dihmeetlem1N  39311  dihmeetlem13N  39340  iunrelexpmin1  41323