Theorem simplr3 1046

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

Assertion

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

Proof of Theorem simplr3

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

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

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 985

This theorem is referenced by:  netap  7408  prarloclemlt  7648  prarloclemlo  7649  ccatswrd  11168  pfxccat3  11232  resqrexlemdecn  11489  summodclem2  11859  isumss2  11870  pcdvdstr  12816  ennnfoneleminc  12948  prdssgrpd  13414  prdsmndd  13447  grprcan  13536  mulgnn0dir  13655  mulgdir  13657  mulgass  13662  lmodprop2d  14277  lssintclm  14313  psrbaglesuppg  14601  restopnb  14820  blsscls2  15132