Theorem simplr3 1072

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

Assertion

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

Proof of Theorem simplr3

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

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

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 1011

This theorem is referenced by:  netap  7614  prarloclemlt  7854  prarloclemlo  7855  ccatswrd  11425  pfxccat3  11489  resqrexlemdecn  11761  summodclem2  12132  isumss2  12143  pcdvdstr  13089  ennnfoneleminc  13285  grprcan  13825  mulgnn0dir  13938  mulgdir  13940  mulgass  13945  prdssgrpd  14174  prdsmndd  14177  lmodprop2d  14668  lssintclm  14704  psrbaglesuppg  15040  restopnb  15265  blsscls2  15577