Theorem andiff

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

	Ref	Expression
Hypotheses	andiff.1	|- ( ph -> ( ch -> th ) )
	andiff.2	|- ( ps -> ( th -> ch ) )
Assertion	andiff	|- ( ( ph /\ ps ) -> ( ch <-> th ) )

Proof

Step	Hyp	Ref	Expression
1		andiff.1	|- ( ph -> ( ch -> th ) )
2		andiff.2	|- ( ps -> ( th -> ch ) )
3	1 2	anim12i	|- ( ( ph /\ ps ) -> ( ( ch -> th ) /\ ( th -> ch ) ) )
4		dfbi2	|- ( ( ch <-> th ) <-> ( ( ch -> th ) /\ ( th -> ch ) ) )
5	3 4	sylibr	|- ( ( ph /\ ps ) -> ( ch <-> th ) )