Theorem bnj835 35118

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  bnj1219  35158  bnj1379  35188  bnj1175  35362  bnj1286  35377  bnj1280  35378  bnj1296  35379  bnj1398  35392  bnj1415  35396  bnj1417  35399  bnj1421  35400  bnj1442  35407  bnj1450  35408  bnj1452  35410  bnj1489  35414  bnj1312  35416  bnj1501  35425  bnj1523  35429