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 syl6ibr ⊢φ→ψ→χ→τ↔θ→φ∧ψ∧χ→θ↔τ
9 5 8 impbii ⊢φ∧ψ∧χ→θ↔τ↔φ→ψ→χ→τ↔θ