This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dfvd3

Description: Definition of a 3-hypothesis virtual deduction. (Contributed by Alan Sare, 14-Nov-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion dfvd3 ( (    𝜑    ,    𝜓    ,    𝜒    ▶    𝜃    ) ↔ ( 𝜑 → ( 𝜓 → ( 𝜒 → 𝜃 ) ) ) )

Proof

Step Hyp Ref Expression
1 df-vd3 ⊢ ( (    𝜑    ,    𝜓    ,    𝜒    ▶    𝜃    ) ↔ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) → 𝜃 ) )
2 df-3an ⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) )
3 2 imbi1i ⊢ ( ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) → 𝜃 ) ↔ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) → 𝜃 ) )
4 impexp ⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) → 𝜃 ) ↔ ( ( 𝜑 ∧ 𝜓 ) → ( 𝜒 → 𝜃 ) ) )
5 3 4 bitri ⊢ ( ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) → 𝜃 ) ↔ ( ( 𝜑 ∧ 𝜓 ) → ( 𝜒 → 𝜃 ) ) )
6 impexp ⊢ ( ( ( 𝜑 ∧ 𝜓 ) → ( 𝜒 → 𝜃 ) ) ↔ ( 𝜑 → ( 𝜓 → ( 𝜒 → 𝜃 ) ) ) )
7 5 6 bitri ⊢ ( ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) → 𝜃 ) ↔ ( 𝜑 → ( 𝜓 → ( 𝜒 → 𝜃 ) ) ) )
8 1 7 bitri ⊢ ( (    𝜑    ,    𝜓    ,    𝜒    ▶    𝜃    ) ↔ ( 𝜑 → ( 𝜓 → ( 𝜒 → 𝜃 ) ) ) )