Theorem sylibda

Description: A syllogism deduction. (Contributed by SN, 16-Jul-2024)

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

Proof

Step	Hyp	Ref	Expression
1		sylibda.1	|- ( ph -> ( ps <-> ch ) )
2		sylibda.2	|- ( ( ph /\ ch ) -> th )
3	1	biimpa	|- ( ( ph /\ ps ) -> ch )
4	3 2	syldan	|- ( ( ph /\ ps ) -> th )