Theorem bnj835 35057

Description: ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)

Hypotheses

Ref	Expression
bnj835.1	⊢ (𝜂 ↔ (𝜑 ∧ 𝜓 ∧ 𝜒))
bnj835.2	⊢ (𝜑 → 𝜏)

Assertion

Ref	Expression
bnj835	⊢ (𝜂 → 𝜏)

Proof of Theorem bnj835

Step	Hyp	Ref	Expression
1		bnj835.1	. 2 ⊢ (𝜂 ↔ (𝜑 ∧ 𝜓 ∧ 𝜒))
2		bnj835.2	. . 3 ⊢ (𝜑 → 𝜏)
3	2	3ad2ant1 1147	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜏)
4	1, 3	sylbi 219	1 ⊢ (𝜂 → 𝜏)

Syntax hints:   → wi 4   ↔ wb 208   ∧ w3a 1099

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 209  df-an 400  df-3an 1101

This theorem is referenced by:  bnj1219  35097  bnj1379  35127  bnj1175  35301  bnj1286  35316  bnj1280  35317  bnj1296  35318  bnj1398  35331  bnj1415  35335  bnj1417  35338  bnj1421  35339  bnj1442  35346  bnj1450  35347  bnj1452  35349  bnj1489  35353  bnj1312  35355  bnj1501  35364  bnj1523  35368