Theorem simp2rr 1244

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 1134	1 ⊢ ((𝜃 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏) → 𝜓)

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

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  fpr3g  8264  tfrlem5  8348  omeu  8549  gruina  10771  4sqlem18  16933  vdwlem10  16961  mdetuni0  22508  mdetmul  22510  tsmsxp  24042  ax5seglem3  28858  btwnconn1lem1  36075  btwnconn1lem3  36077  btwnconn1lem4  36078  btwnconn1lem5  36079  btwnconn1lem6  36080  btwnconn1lem7  36081  btwnconn1lem12  36086  linethru  36141  2llnjN  39561  2lplnja  39613  2lplnj  39614  cdlemblem  39787  dalaw  39880  pclfinN  39894  lhpmcvr4N  40020  cdlemb2  40035  cdleme01N  40215  cdleme0ex2N  40218  cdleme7c  40239  cdlemefrs29bpre0  40390  cdlemefrs29cpre1  40392  cdlemefrs32fva1  40395  cdlemefs32sn1aw  40408  cdleme41sn3a  40427  cdleme48fv  40493  cdlemk21-2N  40885  dihmeetlem13N  41313  pellex  42823  lmhmfgsplit  43075  iunrelexpmin1  43697