Metamath Proof Explorer


Theorem retbwax3

Description: tbw-ax3 rederived from merco1 . (Contributed by Anthony Hart, 17-Sep-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion retbwax3 ( ( ( 𝜑𝜓 ) → 𝜑 ) → 𝜑 )

Proof

Step Hyp Ref Expression
1 retbwax2 ( 𝜑 → ( 𝜑𝜑 ) )
2 merco1lem7 ( ( 𝜑 → ( 𝜑𝜑 ) ) → ( ( ( 𝜑𝜓 ) → 𝜑 ) → 𝜑 ) )
3 1 2 ax-mp ( ( ( 𝜑𝜓 ) → 𝜑 ) → 𝜑 )