Theorem simp2lr 1243

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

Assertion

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

Proof of Theorem simp2lr

Step	Hyp	Ref	Expression
1		simplr 769	. 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  8228  tfrlem5  8312  omeu  8513  expmordi  14120  4sqlem18  16924  vdwlem10  16952  mvrf1  21974  mdetuni0  22596  mdetmul  22598  tsmsxp  24130  ax5seglem3  29014  btwnconn1lem1  36285  btwnconn1lem3  36287  btwnconn1lem4  36288  btwnconn1lem5  36289  btwnconn1lem6  36290  btwnconn1lem7  36291  linethru  36351  lshpkrlem6  39575  athgt  39916  2llnjN  40027  dalaw  40346  cdlemb2  40501  4atexlemex6  40534  cdleme01N  40681  cdleme0ex2N  40684  cdleme7aa  40702  cdleme7e  40707  cdlemg33c0  41162  dihmeetlem3N  41765  pellex  43281