Theorem simp2rl 1238

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

Assertion

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

Proof of Theorem simp2rl

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  tfrlem5  8015  omeu  8210  wemaplem3  9011  gruina  10239  expmordi  13530  4sqlem18  16297  vdwlem10  16325  mdetuni0  21229  mdetmul  21231  tsmsxp  22762  ax5seglem3  26716  btwnconn1lem1  33548  btwnconn1lem2  33549  btwnconn1lem3  33550  btwnconn1lem4  33551  btwnconn1lem12  33559  btwnconn1lem13  33560  linethru  33614  2llnjN  36702  2lplnja  36754  2lplnj  36755  cdlemblem  36928  dalaw  37021  pclfinN  37035  lhpmcvr4N  37161  lhp2atne  37169  lhp2at0ne  37171  cdlemb2  37176  cdlemd7  37339  cdleme01N  37356  cdleme02N  37357  cdleme0ex2N  37359  cdleme7aa  37377  cdleme7c  37380  cdleme7d  37381  cdleme7e  37382  cdleme7ga  37383  cdleme11a  37395  cdleme20k  37454  cdleme21d  37465  cdleme27cl  37501  cdlemefrs29bpre0  37531  cdlemefrs29cpre1  37533  cdlemefrs32fva  37535  cdlemefrs32fva1  37536  cdlemefr29exN  37537  cdlemefr32sn2aw  37539  cdlemefr31fv1  37546  cdlemefs32sn1aw  37549  cdlemefr44  37560  cdlemefr45e  37563  cdleme41sn3a  37568  cdleme35a  37583  cdleme35fnpq  37584  cdleme35b  37585  cdleme35c  37586  cdleme35d  37587  cdleme35e  37588  cdleme35f  37589  cdleme35sn3a  37594  cdleme42e  37614  cdleme42h  37617  cdleme42i  37618  cdleme17d2  37630  cdleme48fv  37634  cdleme48bw  37637  cdleme48b  37638  cdlemeg46c  37648  cdlemeg46ngfr  37653  cdleme48d  37670  cdlemg2kq  37737  cdlemg2m  37739  cdlemg7fvN  37759  cdlemg8a  37762  cdlemg11aq  37773  cdlemg10c  37774  cdlemg17a  37796  cdlemg31b0N  37829  cdlemg41  37853  cdlemh2  37951  cdlemi  37955  cdlemk21-2N  38026  dihmeetlem1N  38425  dihmeetlem13N  38454  iunrelexpmin1  40051