Theorem simp2rr 1124

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

Assertion

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

Proof of Theorem simp2rr

Step	Hyp	Ref	Expression
1		simprr 792	. 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  gruina  9519  4sqlem18  15504  vdwlem10  15532  mdetuni0  20246  mdetmul  20248  tsmsxp  21768  ax5seglem3  25611  btwnconn1lem1  31364  btwnconn1lem3  31366  btwnconn1lem4  31367  btwnconn1lem5  31368  btwnconn1lem6  31369  btwnconn1lem7  31370  btwnconn1lem12  31375  linethru  31430  2llnjN  33871  2lplnja  33923  2lplnj  33924  cdlemblem  34097  dalaw  34190  pclfinN  34204  lhpmcvr4N  34330  cdlemb2  34345  cdleme01N  34526  cdleme0ex2N  34529  cdleme7c  34550  cdlemefrs29bpre0  34702  cdlemefrs29cpre1  34704  cdlemefrs32fva1  34707  cdlemefs32sn1aw  34720  cdleme41sn3a  34739  cdleme48fv  34805  cdlemk21-2N  35197  dihmeetlem13N  35626  pellex  36417  lmhmfgsplit  36674  iunrelexpmin1  37019