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 771	. 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓)) → 𝜑)
2	1	3ad2ant2 1135	1 ⊢ ((𝜃 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  tfrlem5  8420  omeu  8623  wemaplem3  9588  gruina  10858  expmordi  14207  4sqlem18  17000  vdwlem10  17028  mdetuni0  22627  mdetmul  22629  tsmsxp  24163  ax5seglem3  28946  btwnconn1lem1  36088  btwnconn1lem2  36089  btwnconn1lem3  36090  btwnconn1lem4  36091  btwnconn1lem12  36099  btwnconn1lem13  36100  linethru  36154  2llnjN  39569  2lplnja  39621  2lplnj  39622  cdlemblem  39795  dalaw  39888  pclfinN  39902  lhpmcvr4N  40028  lhp2atne  40036  lhp2at0ne  40038  cdlemb2  40043  cdlemd7  40206  cdleme01N  40223  cdleme02N  40224  cdleme0ex2N  40226  cdleme7aa  40244  cdleme7c  40247  cdleme7d  40248  cdleme7e  40249  cdleme7ga  40250  cdleme11a  40262  cdleme20k  40321  cdleme21d  40332  cdleme27cl  40368  cdlemefrs29bpre0  40398  cdlemefrs29cpre1  40400  cdlemefrs32fva  40402  cdlemefrs32fva1  40403  cdlemefr29exN  40404  cdlemefr32sn2aw  40406  cdlemefr31fv1  40413  cdlemefs32sn1aw  40416  cdlemefr44  40427  cdlemefr45e  40430  cdleme41sn3a  40435  cdleme35a  40450  cdleme35fnpq  40451  cdleme35b  40452  cdleme35c  40453  cdleme35d  40454  cdleme35e  40455  cdleme35f  40456  cdleme35sn3a  40461  cdleme42e  40481  cdleme42h  40484  cdleme42i  40485  cdleme17d2  40497  cdleme48fv  40501  cdleme48bw  40504  cdleme48b  40505  cdlemeg46c  40515  cdlemeg46ngfr  40520  cdleme48d  40537  cdlemg2kq  40604  cdlemg2m  40606  cdlemg7fvN  40626  cdlemg8a  40629  cdlemg11aq  40640  cdlemg10c  40641  cdlemg17a  40663  cdlemg31b0N  40696  cdlemg41  40720  cdlemh2  40818  cdlemi  40822  cdlemk21-2N  40893  dihmeetlem1N  41292  dihmeetlem13N  41321  iunrelexpmin1  43721