Theorem simpr31 1144

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

Assertion

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

Proof of Theorem simpr31

Step	Hyp	Ref	Expression
1		simp31 1090	. 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  cgr3tr4  31329  seglecgr12im  31387  paddasslem9  34132  cdlemd1  34503  cdlemf2  34868  cdlemk34  35216  dihmeetlem18N  35631  dihmeetlem19N  35632