Theorem simp2rr 1262

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

Assertion

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

Proof of Theorem simp2rr

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  fpr3g  8307  tfrlem5  8391  omeu  8597  gruina  10907  4sqlem18  17146  vdwlem10  17174  mdetuni0  22942  mdetmul  22944  tsmsxp  24480  ax5seglem3  29515  btwnconn1lem1  36945  btwnconn1lem3  36947  btwnconn1lem4  36948  btwnconn1lem5  36949  btwnconn1lem6  36950  btwnconn1lem7  36951  btwnconn1lem12  36956  linethru  37011  2llnjN  40718  2lplnja  40770  2lplnj  40771  cdlemblem  40944  dalaw  41037  pclfinN  41051  lhpmcvr4N  41177  cdlemb2  41192  cdleme01N  41372  cdleme0ex2N  41375  cdleme7c  41396  cdlemefrs29bpre0  41547  cdlemefrs29cpre1  41549  cdlemefrs32fva1  41552  cdlemefs32sn1aw  41565  cdleme41sn3a  41584  cdleme48fv  41650  cdlemk21-2N  42042  dihmeetlem13N  42470  pellex  43936  lmhmfgsplit  44182  iunrelexpmin1  44802