Theorem simp2rl 1123

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

Assertion

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

Proof of Theorem simp2rl

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  tfrlem5  7363  omeu  7552  wemaplem3  8336  gruina  9519  4sqlem18  15504  vdwlem10  15532  mdetuni0  20246  mdetmul  20248  tsmsxp  21768  ax5seglem3  25611  btwnconn1lem1  31364  btwnconn1lem2  31365  btwnconn1lem3  31366  btwnconn1lem4  31367  btwnconn1lem12  31375  btwnconn1lem13  31376  linethru  31430  2llnjN  33871  2lplnja  33923  2lplnj  33924  cdlemblem  34097  dalaw  34190  pclfinN  34204  lhpmcvr4N  34330  lhp2atne  34338  lhp2at0ne  34340  cdlemb2  34345  cdlemd7  34509  cdleme01N  34526  cdleme02N  34527  cdleme0ex2N  34529  cdleme7aa  34547  cdleme7c  34550  cdleme7d  34551  cdleme7e  34552  cdleme7ga  34553  cdleme11a  34565  cdleme20k  34625  cdleme21d  34636  cdleme27cl  34672  cdlemefrs29bpre0  34702  cdlemefrs29cpre1  34704  cdlemefrs32fva  34706  cdlemefrs32fva1  34707  cdlemefr29exN  34708  cdlemefr32sn2aw  34710  cdlemefr31fv1  34717  cdlemefs32sn1aw  34720  cdlemefr44  34731  cdlemefr45e  34734  cdleme41sn3a  34739  cdleme35a  34754  cdleme35fnpq  34755  cdleme35b  34756  cdleme35c  34757  cdleme35d  34758  cdleme35e  34759  cdleme35f  34760  cdleme35sn3a  34765  cdleme42e  34785  cdleme42h  34788  cdleme42i  34789  cdleme17d2  34801  cdleme48fv  34805  cdleme48bw  34808  cdleme48b  34809  cdlemeg46c  34819  cdlemeg46ngfr  34824  cdleme48d  34841  cdlemg2kq  34908  cdlemg2m  34910  cdlemg7fvN  34930  cdlemg8a  34933  cdlemg11aq  34944  cdlemg10c  34945  cdlemg17a  34967  cdlemg31b0N  35000  cdlemg41  35024  cdlemh2  35122  cdlemi  35126  cdlemk21-2N  35197  dihmeetlem1N  35597  dihmeetlem13N  35626  expmordi  36530  iunrelexpmin1  37019