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  8311  omeu  8512  wemaplem3  9453  gruina  10729  expmordi  14090  4sqlem18  16890  vdwlem10  16918  mdetuni0  22565  mdetmul  22567  tsmsxp  24099  ax5seglem3  29004  btwnconn1lem1  36281  btwnconn1lem2  36282  btwnconn1lem3  36283  btwnconn1lem4  36284  btwnconn1lem12  36292  btwnconn1lem13  36293  linethru  36347  2llnjN  39823  2lplnja  39875  2lplnj  39876  cdlemblem  40049  dalaw  40142  pclfinN  40156  lhpmcvr4N  40282  lhp2atne  40290  lhp2at0ne  40292  cdlemb2  40297  cdlemd7  40460  cdleme01N  40477  cdleme02N  40478  cdleme0ex2N  40480  cdleme7aa  40498  cdleme7c  40501  cdleme7d  40502  cdleme7e  40503  cdleme7ga  40504  cdleme11a  40516  cdleme20k  40575  cdleme21d  40586  cdleme27cl  40622  cdlemefrs29bpre0  40652  cdlemefrs29cpre1  40654  cdlemefrs32fva  40656  cdlemefrs32fva1  40657  cdlemefr29exN  40658  cdlemefr32sn2aw  40660  cdlemefr31fv1  40667  cdlemefs32sn1aw  40670  cdlemefr44  40681  cdlemefr45e  40684  cdleme41sn3a  40689  cdleme35a  40704  cdleme35fnpq  40705  cdleme35b  40706  cdleme35c  40707  cdleme35d  40708  cdleme35e  40709  cdleme35f  40710  cdleme35sn3a  40715  cdleme42e  40735  cdleme42h  40738  cdleme42i  40739  cdleme17d2  40751  cdleme48fv  40755  cdleme48bw  40758  cdleme48b  40759  cdlemeg46c  40769  cdlemeg46ngfr  40774  cdleme48d  40791  cdlemg2kq  40858  cdlemg2m  40860  cdlemg7fvN  40880  cdlemg8a  40883  cdlemg11aq  40894  cdlemg10c  40895  cdlemg17a  40917  cdlemg31b0N  40950  cdlemg41  40974  cdlemh2  41072  cdlemi  41076  cdlemk21-2N  41147  dihmeetlem1N  41546  dihmeetlem13N  41575  iunrelexpmin1  43945