Metamath Proof Explorer


Theorem e1bir

Description: Right biconditional form of e1a . sylibr is e1bir without virtual deductions. (Contributed by Alan Sare, 24-Jun-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses e1bir.1 (    𝜑    ▶    𝜓    )
e1bir.2 ( 𝜒𝜓 )
Assertion e1bir (    𝜑    ▶    𝜒    )

Proof

Step Hyp Ref Expression
1 e1bir.1 (    𝜑    ▶    𝜓    )
2 e1bir.2 ( 𝜒𝜓 )
3 2 biimpri ( 𝜓𝜒 )
4 1 3 e1a (    𝜑    ▶    𝜒    )