Theorem andiff

Description: Adding biconditional when antecedents are conjuncted. (Contributed by metakunt, 16-Apr-2024)

	Ref	Expression
Hypotheses	andiff.1	⊢ ( 𝜑 → ( 𝜒 → 𝜃 ) )
	andiff.2	⊢ ( 𝜓 → ( 𝜃 → 𝜒 ) )
Assertion	andiff	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝜒 ↔ 𝜃 ) )

Proof

Step	Hyp	Ref	Expression
1		andiff.1	⊢ ( 𝜑 → ( 𝜒 → 𝜃 ) )
2		andiff.2	⊢ ( 𝜓 → ( 𝜃 → 𝜒 ) )
3	1 2	anim12i	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝜒 → 𝜃 ) ∧ ( 𝜃 → 𝜒 ) ) )
4		dfbi2	⊢ ( ( 𝜒 ↔ 𝜃 ) ↔ ( ( 𝜒 → 𝜃 ) ∧ ( 𝜃 → 𝜒 ) ) )
5	3 4	sylibr	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝜒 ↔ 𝜃 ) )