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

Metamath Proof Explorer

Theorem e3bi

Description: Biconditional form of e3 . syl8ib is e3bi without virtual deductions. (Contributed by Alan Sare, 15-Jun-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses e3bi.1 ⊢ (    𝜑    ,    𝜓    ,    𝜒    ▶    𝜃    )
e3bi.2 ⊢ ( 𝜃 ↔ 𝜏 )
Assertion e3bi (    𝜑    ,    𝜓    ,    𝜒    ▶    𝜏    )

Proof

Step Hyp Ref Expression
1 e3bi.1 ⊢ (    𝜑    ,    𝜓    ,    𝜒    ▶    𝜃    )
2 e3bi.2 ⊢ ( 𝜃 ↔ 𝜏 )
3 2 biimpi ⊢ ( 𝜃 → 𝜏 )
4 1 3 e3 ⊢ (    𝜑    ,    𝜓    ,    𝜒    ▶    𝜏    )