Theorem biimp3a

Description: Infer implication from a logical equivalence. Similar to biimpa . (Contributed by NM, 4-Sep-2005)

	Ref	Expression
Hypothesis	biimp3a.1	|- ( ( ph /\ ps ) -> ( ch <-> th ) )
Assertion	biimp3a	|- ( ( ph /\ ps /\ ch ) -> th )

Proof

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