Theorem simpr32 1145

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

Assertion

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

Proof of Theorem simpr32

Step	Hyp	Ref	Expression
1		simp32 1091	. 2 ⊢ ((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) → 𝜓)
2	1	adantl 481	1 ⊢ ((𝜂 ∧ (𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  oppccatid  16202  subccatid  16329  fuccatid  16452  setccatid  16557  catccatid  16575  estrccatid  16595  xpccatid  16651  nllyidm  21102  utoptop  21848  omndmul2  29043  cgr3tr4  31329  paddasslem9  34132  cdlemd1  34503  cdlemf2  34868  cdlemk34  35216  dihmeetlem18N  35631