Metamath Proof Explorer

Theorem 3impexpbicom

Description: Version of 3impexp where in addition the consequent is commuted. (Contributed by Alan Sare, 31-Dec-2011)

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

Proof

Step Hyp Ref Expression
1 bicom ⊢ θ ↔ τ ↔ τ ↔ θ
2 imbi2 ⊢ θ ↔ τ ↔ τ ↔ θ → φ ∧ ψ ∧ χ → θ ↔ τ ↔ φ ∧ ψ ∧ χ → τ ↔ θ
3 2 biimpcd ⊢ φ ∧ ψ ∧ χ → θ ↔ τ → θ ↔ τ ↔ τ ↔ θ → φ ∧ ψ ∧ χ → τ ↔ θ
4 1 3 mpi ⊢ φ ∧ ψ ∧ χ → θ ↔ τ → φ ∧ ψ ∧ χ → τ ↔ θ
5 4 3expd ⊢ φ ∧ ψ ∧ χ → θ ↔ τ → φ → ψ → χ → τ ↔ θ
6 3impexp ⊢ φ ∧ ψ ∧ χ → τ ↔ θ ↔ φ → ψ → χ → τ ↔ θ
7 6 biimpri ⊢ φ → ψ → χ → τ ↔ θ → φ ∧ ψ ∧ χ → τ ↔ θ
8 7 1 imbitrrdi ⊢ φ → ψ → χ → τ ↔ θ → φ ∧ ψ ∧ χ → θ ↔ τ
9 5 8 impbii ⊢ φ ∧ ψ ∧ χ → θ ↔ τ ↔ φ → ψ → χ → τ ↔ θ