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 784	. 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓)) → 𝜓)
2	1	3ad2ant2 1152	1 ⊢ ((𝜃 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  fpr3g  8283  tfrlem5  8367  omeu  8571  gruina  10804  4sqlem18  17023  vdwlem10  17051  mdetuni0  22759  mdetmul  22761  tsmsxp  24293  ax5seglem3  29262  btwnconn1lem1  36560  btwnconn1lem3  36562  btwnconn1lem4  36563  btwnconn1lem5  36564  btwnconn1lem6  36565  btwnconn1lem7  36566  btwnconn1lem12  36571  linethru  36626  2llnjN  40322  2lplnja  40374  2lplnj  40375  cdlemblem  40548  dalaw  40641  pclfinN  40655  lhpmcvr4N  40781  cdlemb2  40796  cdleme01N  40976  cdleme0ex2N  40979  cdleme7c  41000  cdlemefrs29bpre0  41151  cdlemefrs29cpre1  41153  cdlemefrs32fva1  41156  cdlemefs32sn1aw  41169  cdleme41sn3a  41188  cdleme48fv  41254  cdlemk21-2N  41646  dihmeetlem13N  42074  pellex  43545  lmhmfgsplit  43796  iunrelexpmin1  44417