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 771	. 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓)) → 𝜑)
2	1	3ad2ant2 1133	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  8419  omeu  8622  wemaplem3  9586  gruina  10856  expmordi  14204  4sqlem18  16996  vdwlem10  17024  mdetuni0  22643  mdetmul  22645  tsmsxp  24179  ax5seglem3  28961  btwnconn1lem1  36069  btwnconn1lem2  36070  btwnconn1lem3  36071  btwnconn1lem4  36072  btwnconn1lem12  36080  btwnconn1lem13  36081  linethru  36135  2llnjN  39550  2lplnja  39602  2lplnj  39603  cdlemblem  39776  dalaw  39869  pclfinN  39883  lhpmcvr4N  40009  lhp2atne  40017  lhp2at0ne  40019  cdlemb2  40024  cdlemd7  40187  cdleme01N  40204  cdleme02N  40205  cdleme0ex2N  40207  cdleme7aa  40225  cdleme7c  40228  cdleme7d  40229  cdleme7e  40230  cdleme7ga  40231  cdleme11a  40243  cdleme20k  40302  cdleme21d  40313  cdleme27cl  40349  cdlemefrs29bpre0  40379  cdlemefrs29cpre1  40381  cdlemefrs32fva  40383  cdlemefrs32fva1  40384  cdlemefr29exN  40385  cdlemefr32sn2aw  40387  cdlemefr31fv1  40394  cdlemefs32sn1aw  40397  cdlemefr44  40408  cdlemefr45e  40411  cdleme41sn3a  40416  cdleme35a  40431  cdleme35fnpq  40432  cdleme35b  40433  cdleme35c  40434  cdleme35d  40435  cdleme35e  40436  cdleme35f  40437  cdleme35sn3a  40442  cdleme42e  40462  cdleme42h  40465  cdleme42i  40466  cdleme17d2  40478  cdleme48fv  40482  cdleme48bw  40485  cdleme48b  40486  cdlemeg46c  40496  cdlemeg46ngfr  40501  cdleme48d  40518  cdlemg2kq  40585  cdlemg2m  40587  cdlemg7fvN  40607  cdlemg8a  40610  cdlemg11aq  40621  cdlemg10c  40622  cdlemg17a  40644  cdlemg31b0N  40677  cdlemg41  40701  cdlemh2  40799  cdlemi  40803  cdlemk21-2N  40874  dihmeetlem1N  41273  dihmeetlem13N  41302  iunrelexpmin1  43698