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 φ ψ χ θ τ φ ψ χ τ θ