Theorem simp2rl 1244

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  8321  omeu  8522  wemaplem3  9465  gruina  10741  expmordi  14102  4sqlem18  16902  vdwlem10  16930  mdetuni0  22577  mdetmul  22579  tsmsxp  24111  ax5seglem3  29016  btwnconn1lem1  36300  btwnconn1lem2  36301  btwnconn1lem3  36302  btwnconn1lem4  36303  btwnconn1lem12  36311  btwnconn1lem13  36312  linethru  36366  2llnjN  39937  2lplnja  39989  2lplnj  39990  cdlemblem  40163  dalaw  40256  pclfinN  40270  lhpmcvr4N  40396  lhp2atne  40404  lhp2at0ne  40406  cdlemb2  40411  cdlemd7  40574  cdleme01N  40591  cdleme02N  40592  cdleme0ex2N  40594  cdleme7aa  40612  cdleme7c  40615  cdleme7d  40616  cdleme7e  40617  cdleme7ga  40618  cdleme11a  40630  cdleme20k  40689  cdleme21d  40700  cdleme27cl  40736  cdlemefrs29bpre0  40766  cdlemefrs29cpre1  40768  cdlemefrs32fva  40770  cdlemefrs32fva1  40771  cdlemefr29exN  40772  cdlemefr32sn2aw  40774  cdlemefr31fv1  40781  cdlemefs32sn1aw  40784  cdlemefr44  40795  cdlemefr45e  40798  cdleme41sn3a  40803  cdleme35a  40818  cdleme35fnpq  40819  cdleme35b  40820  cdleme35c  40821  cdleme35d  40822  cdleme35e  40823  cdleme35f  40824  cdleme35sn3a  40829  cdleme42e  40849  cdleme42h  40852  cdleme42i  40853  cdleme17d2  40865  cdleme48fv  40869  cdleme48bw  40872  cdleme48b  40873  cdlemeg46c  40883  cdlemeg46ngfr  40888  cdleme48d  40905  cdlemg2kq  40972  cdlemg2m  40974  cdlemg7fvN  40994  cdlemg8a  40997  cdlemg11aq  41008  cdlemg10c  41009  cdlemg17a  41031  cdlemg31b0N  41064  cdlemg41  41088  cdlemh2  41186  cdlemi  41190  cdlemk21-2N  41261  dihmeetlem1N  41660  dihmeetlem13N  41689  iunrelexpmin1  44058