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

Metamath Proof Explorer

Theorem 3impexpbicomi

Description: Inference associated with 3impexpbicom . Derived automatically from 3impexpbicomiVD . (Contributed by Alan Sare, 31-Dec-2011)

Ref Expression
Hypothesis 3impexpbicomi.1 ⊢ φ ∧ ψ ∧ χ → θ ↔ τ
Assertion 3impexpbicomi ⊢ φ → ψ → χ → τ ↔ θ

Proof

Step Hyp Ref Expression
1 3impexpbicomi.1 ⊢ φ ∧ ψ ∧ χ → θ ↔ τ
2 1 bicomd ⊢ φ ∧ ψ ∧ χ → τ ↔ θ
3 2 3exp ⊢ φ → ψ → χ → τ ↔ θ