Theorem simpr33 1153

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

Assertion

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

Proof of Theorem simpr33

Step	Hyp	Ref	Expression
1		simp33 1099	. 2 ⊢ ((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) → 𝜒)
2	1	adantl 482	1 ⊢ ((𝜂 ∧ (𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  oppccatid  16379  subccatid  16506  fuccatid  16629  setccatid  16734  catccatid  16752  estrccatid  16772  xpccatid  16828  nllyidm  21292  utoptop  22038  cgr3tr4  32159  paddasslem9  35114  cdlemd1  35485  cdlemf2  35850  cdlemk34  36198  dihmeetlem18N  36613  dihmeetlem19N  36614