Metamath Proof Explorer


Theorem biadanid

Description: Deduction associated with biadani . Add a conjunction to an equivalence. (Contributed by Thierry Arnoux, 16-Jun-2024)

Ref Expression
Hypotheses biadanid.1 ( ( 𝜑𝜓 ) → 𝜒 )
biadanid.2 ( ( 𝜑𝜒 ) → ( 𝜓𝜃 ) )
Assertion biadanid ( 𝜑 → ( 𝜓 ↔ ( 𝜒𝜃 ) ) )

Proof

Step Hyp Ref Expression
1 biadanid.1 ( ( 𝜑𝜓 ) → 𝜒 )
2 biadanid.2 ( ( 𝜑𝜒 ) → ( 𝜓𝜃 ) )
3 2 biimpa ( ( ( 𝜑𝜒 ) ∧ 𝜓 ) → 𝜃 )
4 3 an32s ( ( ( 𝜑𝜓 ) ∧ 𝜒 ) → 𝜃 )
5 1 4 mpdan ( ( 𝜑𝜓 ) → 𝜃 )
6 1 5 jca ( ( 𝜑𝜓 ) → ( 𝜒𝜃 ) )
7 2 biimpar ( ( ( 𝜑𝜒 ) ∧ 𝜃 ) → 𝜓 )
8 7 anasss ( ( 𝜑 ∧ ( 𝜒𝜃 ) ) → 𝜓 )
9 6 8 impbida ( 𝜑 → ( 𝜓 ↔ ( 𝜒𝜃 ) ) )