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  8375  omeu  8579  wemaplem3  9520  gruina  10821  expmordi  14223  4sqlem18  17047  vdwlem10  17075  mdetuni0  22815  mdetmul  22817  tsmsxp  24349  ax5seglem3  29318  btwnconn1lem1  36600  btwnconn1lem2  36601  btwnconn1lem3  36602  btwnconn1lem4  36603  btwnconn1lem12  36611  btwnconn1lem13  36612  linethru  36666  2llnjN  40382  2lplnja  40434  2lplnj  40435  cdlemblem  40608  dalaw  40701  pclfinN  40715  lhpmcvr4N  40841  lhp2atne  40849  lhp2at0ne  40851  cdlemb2  40856  cdlemd7  41019  cdleme01N  41036  cdleme02N  41037  cdleme0ex2N  41039  cdleme7aa  41057  cdleme7c  41060  cdleme7d  41061  cdleme7e  41062  cdleme7ga  41063  cdleme11a  41075  cdleme20k  41134  cdleme21d  41145  cdleme27cl  41181  cdlemefrs29bpre0  41211  cdlemefrs29cpre1  41213  cdlemefrs32fva  41215  cdlemefrs32fva1  41216  cdlemefr29exN  41217  cdlemefr32sn2aw  41219  cdlemefr31fv1  41226  cdlemefs32sn1aw  41229  cdlemefr44  41240  cdlemefr45e  41243  cdleme41sn3a  41248  cdleme35a  41263  cdleme35fnpq  41264  cdleme35b  41265  cdleme35c  41266  cdleme35d  41267  cdleme35e  41268  cdleme35f  41269  cdleme35sn3a  41274  cdleme42e  41294  cdleme42h  41297  cdleme42i  41298  cdleme17d2  41310  cdleme48fv  41314  cdleme48bw  41317  cdleme48b  41318  cdlemeg46c  41328  cdlemeg46ngfr  41333  cdleme48d  41350  cdlemg2kq  41417  cdlemg2m  41419  cdlemg7fvN  41439  cdlemg8a  41442  cdlemg11aq  41453  cdlemg10c  41454  cdlemg17a  41476  cdlemg31b0N  41509  cdlemg41  41533  cdlemh2  41631  cdlemi  41635  cdlemk21-2N  41706  dihmeetlem1N  42105  dihmeetlem13N  42134  iunrelexpmin1  44475