Theorem simp2rl 1235

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Assertion

Ref	Expression
simp2rl	⊢ ((𝜃 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏) → 𝜑)

Proof of Theorem simp2rl

Step	Hyp	Ref	Expression
1		simprl 767	. 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓)) → 𝜑)
2	1	3ad2ant2 1127	1 ⊢ ((𝜃 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1080

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 208  df-an 397  df-3an 1082

This theorem is referenced by:  tfrlem5  7875  omeu  8068  wemaplem3  8865  gruina  10093  expmordi  13385  4sqlem18  16131  vdwlem10  16159  mdetuni0  20918  mdetmul  20920  tsmsxp  22450  ax5seglem3  26404  btwnconn1lem1  33159  btwnconn1lem2  33160  btwnconn1lem3  33161  btwnconn1lem4  33162  btwnconn1lem12  33170  btwnconn1lem13  33171  linethru  33225  2llnjN  36255  2lplnja  36307  2lplnj  36308  cdlemblem  36481  dalaw  36574  pclfinN  36588  lhpmcvr4N  36714  lhp2atne  36722  lhp2at0ne  36724  cdlemb2  36729  cdlemd7  36892  cdleme01N  36909  cdleme02N  36910  cdleme0ex2N  36912  cdleme7aa  36930  cdleme7c  36933  cdleme7d  36934  cdleme7e  36935  cdleme7ga  36936  cdleme11a  36948  cdleme20k  37007  cdleme21d  37018  cdleme27cl  37054  cdlemefrs29bpre0  37084  cdlemefrs29cpre1  37086  cdlemefrs32fva  37088  cdlemefrs32fva1  37089  cdlemefr29exN  37090  cdlemefr32sn2aw  37092  cdlemefr31fv1  37099  cdlemefs32sn1aw  37102  cdlemefr44  37113  cdlemefr45e  37116  cdleme41sn3a  37121  cdleme35a  37136  cdleme35fnpq  37137  cdleme35b  37138  cdleme35c  37139  cdleme35d  37140  cdleme35e  37141  cdleme35f  37142  cdleme35sn3a  37147  cdleme42e  37167  cdleme42h  37170  cdleme42i  37171  cdleme17d2  37183  cdleme48fv  37187  cdleme48bw  37190  cdleme48b  37191  cdlemeg46c  37201  cdlemeg46ngfr  37206  cdleme48d  37223  cdlemg2kq  37290  cdlemg2m  37292  cdlemg7fvN  37312  cdlemg8a  37315  cdlemg11aq  37326  cdlemg10c  37327  cdlemg17a  37349  cdlemg31b0N  37382  cdlemg41  37406  cdlemh2  37504  cdlemi  37508  cdlemk21-2N  37579  dihmeetlem1N  37978  dihmeetlem13N  38007  iunrelexpmin1  39559