Metamath Proof Explorer


Theorem 3anibar

Description: Remove a hypothesis from the second member of a biconditional. (Contributed by FL, 22-Jul-2008)

Ref Expression
Hypothesis 3anibar.1 ( ( 𝜑𝜓𝜒 ) → ( 𝜃 ↔ ( 𝜒𝜏 ) ) )
Assertion 3anibar ( ( 𝜑𝜓𝜒 ) → ( 𝜃𝜏 ) )

Proof

Step Hyp Ref Expression
1 3anibar.1 ( ( 𝜑𝜓𝜒 ) → ( 𝜃 ↔ ( 𝜒𝜏 ) ) )
2 simp3 ( ( 𝜑𝜓𝜒 ) → 𝜒 )
3 2 1 mpbirand ( ( 𝜑𝜓𝜒 ) → ( 𝜃𝜏 ) )