Metamath Proof Explorer


Theorem anbi1cd

Description: Introduce a proposition as left conjunct on the left-hand side and right conjunct on the right-hand side of an equivalence. Deduction form. (Contributed by Peter Mazsa, 22-May-2021)

Ref Expression
Hypothesis anbi1cd.1 ( 𝜑 → ( 𝜓𝜒 ) )
Assertion anbi1cd ( 𝜑 → ( ( 𝜃𝜓 ) ↔ ( 𝜒𝜃 ) ) )

Proof

Step Hyp Ref Expression
1 anbi1cd.1 ( 𝜑 → ( 𝜓𝜒 ) )
2 1 anbi2d ( 𝜑 → ( ( 𝜃𝜓 ) ↔ ( 𝜃𝜒 ) ) )
3 2 biancomd ( 𝜑 → ( ( 𝜃𝜓 ) ↔ ( 𝜒𝜃 ) ) )