Theorem simp2rl 1243

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

Assertion

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

Proof of Theorem simp2rl

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1088

This theorem is referenced by:  tfrlem5  8309  omeu  8510  wemaplem3  9459  gruina  10731  expmordi  14092  4sqlem18  16892  vdwlem10  16920  mdetuni0  22524  mdetmul  22526  tsmsxp  24058  ax5seglem3  28894  btwnconn1lem1  36060  btwnconn1lem2  36061  btwnconn1lem3  36062  btwnconn1lem4  36063  btwnconn1lem12  36071  btwnconn1lem13  36072  linethru  36126  2llnjN  39546  2lplnja  39598  2lplnj  39599  cdlemblem  39772  dalaw  39865  pclfinN  39879  lhpmcvr4N  40005  lhp2atne  40013  lhp2at0ne  40015  cdlemb2  40020  cdlemd7  40183  cdleme01N  40200  cdleme02N  40201  cdleme0ex2N  40203  cdleme7aa  40221  cdleme7c  40224  cdleme7d  40225  cdleme7e  40226  cdleme7ga  40227  cdleme11a  40239  cdleme20k  40298  cdleme21d  40309  cdleme27cl  40345  cdlemefrs29bpre0  40375  cdlemefrs29cpre1  40377  cdlemefrs32fva  40379  cdlemefrs32fva1  40380  cdlemefr29exN  40381  cdlemefr32sn2aw  40383  cdlemefr31fv1  40390  cdlemefs32sn1aw  40393  cdlemefr44  40404  cdlemefr45e  40407  cdleme41sn3a  40412  cdleme35a  40427  cdleme35fnpq  40428  cdleme35b  40429  cdleme35c  40430  cdleme35d  40431  cdleme35e  40432  cdleme35f  40433  cdleme35sn3a  40438  cdleme42e  40458  cdleme42h  40461  cdleme42i  40462  cdleme17d2  40474  cdleme48fv  40478  cdleme48bw  40481  cdleme48b  40482  cdlemeg46c  40492  cdlemeg46ngfr  40497  cdleme48d  40514  cdlemg2kq  40581  cdlemg2m  40583  cdlemg7fvN  40603  cdlemg8a  40606  cdlemg11aq  40617  cdlemg10c  40618  cdlemg17a  40640  cdlemg31b0N  40673  cdlemg41  40697  cdlemh2  40795  cdlemi  40799  cdlemk21-2N  40870  dihmeetlem1N  41269  dihmeetlem13N  41298  iunrelexpmin1  43681