Theorem 3impexpbicom 1367

Description: 3impexp 1366 with biconditional consequent of antecedent that is commuted in consequent. Derived automatically from 3impexpVD in set.mm. (Contributed by Alan Sare, 31-Dec-2011.) (New usage is discouraged.) TODO: decide if this is worth keeping.

Assertion

Ref	Expression
3impexpbicom	⊢ (((φ ∧ ψ ∧ χ) → (θ ↔ τ)) ↔ (φ → (ψ → (χ → (τ ↔ θ)))))

Proof of Theorem 3impexpbicom

Step	Hyp	Ref	Expression
1		bicom 191	. . . 4 ⊢ ((θ ↔ τ) ↔ (τ ↔ θ))
2		imbi2 314	. . . . 5 ⊢ (((θ ↔ τ) ↔ (τ ↔ θ)) → (((φ ∧ ψ ∧ χ) → (θ ↔ τ)) ↔ ((φ ∧ ψ ∧ χ) → (τ ↔ θ))))
3	2	biimpcd 215	. . . 4 ⊢ (((φ ∧ ψ ∧ χ) → (θ ↔ τ)) → (((θ ↔ τ) ↔ (τ ↔ θ)) → ((φ ∧ ψ ∧ χ) → (τ ↔ θ))))
4	1, 3	mpi 16	. . 3 ⊢ (((φ ∧ ψ ∧ χ) → (θ ↔ τ)) → ((φ ∧ ψ ∧ χ) → (τ ↔ θ)))
5	4	3expd 1168	. 2 ⊢ (((φ ∧ ψ ∧ χ) → (θ ↔ τ)) → (φ → (ψ → (χ → (τ ↔ θ)))))
6		3impexp 1366	. . . 4 ⊢ (((φ ∧ ψ ∧ χ) → (τ ↔ θ)) ↔ (φ → (ψ → (χ → (τ ↔ θ)))))
7	6	biimpri 197	. . 3 ⊢ ((φ → (ψ → (χ → (τ ↔ θ)))) → ((φ ∧ ψ ∧ χ) → (τ ↔ θ)))
8	7, 1	syl6ibr 218	. 2 ⊢ ((φ → (ψ → (χ → (τ ↔ θ)))) → ((φ ∧ ψ ∧ χ) → (θ ↔ τ)))
9	5, 8	impbii 180	1 ⊢ (((φ ∧ ψ ∧ χ) → (θ ↔ τ)) ↔ (φ → (ψ → (χ → (τ ↔ θ)))))

This proof depends on syntax axioms:   → wi 4   ↔ wb 176   ∧ w3a 934

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 177  df-an 360  df-3an 936

This theorem is used by: (None)