Theorem sylbida

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

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

Proof

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