Theorem simp2rr 1239

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

Assertion

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

Proof of Theorem simp2rr

Step	Hyp	Ref	Expression
1		simprr 771	. 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  8010  omeu  8205  gruina  10234  4sqlem18  16292  vdwlem10  16320  mdetuni0  21224  mdetmul  21226  tsmsxp  22757  ax5seglem3  26711  fpr3g  33117  btwnconn1lem1  33543  btwnconn1lem3  33545  btwnconn1lem4  33546  btwnconn1lem5  33547  btwnconn1lem6  33548  btwnconn1lem7  33549  btwnconn1lem12  33554  linethru  33609  2llnjN  36697  2lplnja  36749  2lplnj  36750  cdlemblem  36923  dalaw  37016  pclfinN  37030  lhpmcvr4N  37156  cdlemb2  37171  cdleme01N  37351  cdleme0ex2N  37354  cdleme7c  37375  cdlemefrs29bpre0  37526  cdlemefrs29cpre1  37528  cdlemefrs32fva1  37531  cdlemefs32sn1aw  37544  cdleme41sn3a  37563  cdleme48fv  37629  cdlemk21-2N  38021  dihmeetlem13N  38449  pellex  39425  lmhmfgsplit  39679  iunrelexpmin1  40046