Theorem simp2rr 1241

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

Assertion

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

Proof of Theorem simp2rr

Step	Hyp	Ref	Expression
1		simprr 772	. 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓)) → 𝜓)
2	1	3ad2ant2 1132	1 ⊢ ((𝜃 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏) → 𝜓)

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

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  fpr3g  8284  tfrlem5  8394  omeu  8599  gruina  10833  4sqlem18  16922  vdwlem10  16950  mdetuni0  22510  mdetmul  22512  tsmsxp  24046  ax5seglem3  28729  btwnconn1lem1  35619  btwnconn1lem3  35621  btwnconn1lem4  35622  btwnconn1lem5  35623  btwnconn1lem6  35624  btwnconn1lem7  35625  btwnconn1lem12  35630  linethru  35685  2llnjN  38977  2lplnja  39029  2lplnj  39030  cdlemblem  39203  dalaw  39296  pclfinN  39310  lhpmcvr4N  39436  cdlemb2  39451  cdleme01N  39631  cdleme0ex2N  39634  cdleme7c  39655  cdlemefrs29bpre0  39806  cdlemefrs29cpre1  39808  cdlemefrs32fva1  39811  cdlemefs32sn1aw  39824  cdleme41sn3a  39843  cdleme48fv  39909  cdlemk21-2N  40301  dihmeetlem13N  40729  pellex  42177  lmhmfgsplit  42432  iunrelexpmin1  43061