Theorem bnj835 32718

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 1131	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜏)
4	1, 3	sylbi 216	1 ⊢ (𝜂 → 𝜏)

Syntax hints:   → wi 4   ↔ wb 205   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  bnj1219  32759  bnj1379  32789  bnj1175  32963  bnj1286  32978  bnj1280  32979  bnj1296  32980  bnj1398  32993  bnj1415  32997  bnj1417  33000  bnj1421  33001  bnj1442  33008  bnj1450  33009  bnj1452  33011  bnj1489  33015  bnj1312  33017  bnj1501  33026  bnj1523  33030