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  8305  omeu  8506  wemaplem3  9441  gruina  10716  expmordi  14076  4sqlem18  16876  vdwlem10  16904  mdetuni0  22537  mdetmul  22539  tsmsxp  24071  ax5seglem3  28911  btwnconn1lem1  36152  btwnconn1lem2  36153  btwnconn1lem3  36154  btwnconn1lem4  36155  btwnconn1lem12  36163  btwnconn1lem13  36164  linethru  36218  2llnjN  39686  2lplnja  39738  2lplnj  39739  cdlemblem  39912  dalaw  40005  pclfinN  40019  lhpmcvr4N  40145  lhp2atne  40153  lhp2at0ne  40155  cdlemb2  40160  cdlemd7  40323  cdleme01N  40340  cdleme02N  40341  cdleme0ex2N  40343  cdleme7aa  40361  cdleme7c  40364  cdleme7d  40365  cdleme7e  40366  cdleme7ga  40367  cdleme11a  40379  cdleme20k  40438  cdleme21d  40449  cdleme27cl  40485  cdlemefrs29bpre0  40515  cdlemefrs29cpre1  40517  cdlemefrs32fva  40519  cdlemefrs32fva1  40520  cdlemefr29exN  40521  cdlemefr32sn2aw  40523  cdlemefr31fv1  40530  cdlemefs32sn1aw  40533  cdlemefr44  40544  cdlemefr45e  40547  cdleme41sn3a  40552  cdleme35a  40567  cdleme35fnpq  40568  cdleme35b  40569  cdleme35c  40570  cdleme35d  40571  cdleme35e  40572  cdleme35f  40573  cdleme35sn3a  40578  cdleme42e  40598  cdleme42h  40601  cdleme42i  40602  cdleme17d2  40614  cdleme48fv  40618  cdleme48bw  40621  cdleme48b  40622  cdlemeg46c  40632  cdlemeg46ngfr  40637  cdleme48d  40654  cdlemg2kq  40721  cdlemg2m  40723  cdlemg7fvN  40743  cdlemg8a  40746  cdlemg11aq  40757  cdlemg10c  40758  cdlemg17a  40780  cdlemg31b0N  40813  cdlemg41  40837  cdlemh2  40935  cdlemi  40939  cdlemk21-2N  41010  dihmeetlem1N  41409  dihmeetlem13N  41438  iunrelexpmin1  43825