Theorem bnj835 31678

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

Syntax hints:   → wi 4   ↔ wb 198   ∧ w3a 1068

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 199  df-an 388  df-3an 1070

This theorem is referenced by:  bnj1219  31720  bnj1379  31750  bnj1175  31921  bnj1286  31936  bnj1280  31937  bnj1296  31938  bnj1398  31951  bnj1415  31955  bnj1417  31958  bnj1421  31959  bnj1442  31966  bnj1450  31967  bnj1452  31969  bnj1489  31973  bnj1312  31975  bnj1501  31984  bnj1523  31988