Theorem simplr3 1068

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

Assertion

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

Proof of Theorem simplr3

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

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

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 1007

This theorem is referenced by:  netap  7573  prarloclemlt  7813  prarloclemlo  7814  ccatswrd  11370  pfxccat3  11434  resqrexlemdecn  11705  summodclem2  12076  isumss2  12087  pcdvdstr  13033  ennnfoneleminc  13183  prdssgrpd  13649  prdsmndd  13682  grprcan  13771  mulgnn0dir  13890  mulgdir  13892  mulgass  13897  lmodprop2d  14545  lssintclm  14581  psrbaglesuppg  14870  restopnb  15095  blsscls2  15407