Theorem simplr3 1065

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

Assertion

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

Proof of Theorem simplr3

Step	Hyp	Ref	Expression
1		simpr3 1029	. 2 ⊢ ((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) → 𝜒)
2	1	adantr 276	1 ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 1002

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 1004

This theorem is referenced by:  netap  7466  prarloclemlt  7706  prarloclemlo  7707  ccatswrd  11244  pfxccat3  11308  resqrexlemdecn  11566  summodclem2  11936  isumss2  11947  pcdvdstr  12893  ennnfoneleminc  13025  prdssgrpd  13491  prdsmndd  13524  grprcan  13613  mulgnn0dir  13732  mulgdir  13734  mulgass  13739  lmodprop2d  14355  lssintclm  14391  psrbaglesuppg  14679  restopnb  14898  blsscls2  15210