Theorem bnj835 34917

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  bnj1219  34958  bnj1379  34988  bnj1175  35162  bnj1286  35177  bnj1280  35178  bnj1296  35179  bnj1398  35192  bnj1415  35196  bnj1417  35199  bnj1421  35200  bnj1442  35207  bnj1450  35208  bnj1452  35210  bnj1489  35214  bnj1312  35216  bnj1501  35225  bnj1523  35229