Theorem simp2rr 1245

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

Assertion

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

Proof of Theorem simp2rr

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

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

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 1089

This theorem is referenced by:  fpr3g  8237  tfrlem5  8321  omeu  8522  gruina  10741  4sqlem18  16902  vdwlem10  16930  mdetuni0  22577  mdetmul  22579  tsmsxp  24111  ax5seglem3  29016  btwnconn1lem1  36300  btwnconn1lem3  36302  btwnconn1lem4  36303  btwnconn1lem5  36304  btwnconn1lem6  36305  btwnconn1lem7  36306  btwnconn1lem12  36311  linethru  36366  2llnjN  39937  2lplnja  39989  2lplnj  39990  cdlemblem  40163  dalaw  40256  pclfinN  40270  lhpmcvr4N  40396  cdlemb2  40411  cdleme01N  40591  cdleme0ex2N  40594  cdleme7c  40615  cdlemefrs29bpre0  40766  cdlemefrs29cpre1  40768  cdlemefrs32fva1  40771  cdlemefs32sn1aw  40784  cdleme41sn3a  40803  cdleme48fv  40869  cdlemk21-2N  41261  dihmeetlem13N  41689  pellex  43186  lmhmfgsplit  43437  iunrelexpmin1  44058