Theorem bnj835 30083

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

Syntax hints:   → wi 4   ↔ wb 195   ∧ 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:  bnj1219  30125  bnj1379  30155  bnj1175  30326  bnj1286  30341  bnj1280  30342  bnj1296  30343  bnj1398  30356  bnj1415  30360  bnj1417  30363  bnj1421  30364  bnj1442  30371  bnj1450  30372  bnj1452  30374  bnj1489  30378  bnj1312  30380  bnj1501  30389  bnj1523  30393