Theorem mpbir3and

Description: Detach a conjunction of truths in a biconditional. (Contributed by Mario Carneiro, 11-May-2014) (Revised by Mario Carneiro, 9-Jan-2015)

	Ref	Expression
Hypotheses	mpbir3and.1	|- ( ph -> ch )
	mpbir3and.2	|- ( ph -> th )
	mpbir3and.3	|- ( ph -> ta )
	mpbir3and.4	|- ( ph -> ( ps <-> ( ch /\ th /\ ta ) ) )
Assertion	mpbir3and	|- ( ph -> ps )

Proof

Step	Hyp	Ref	Expression
1		mpbir3and.1	|- ( ph -> ch )
2		mpbir3and.2	|- ( ph -> th )
3		mpbir3and.3	|- ( ph -> ta )
4		mpbir3and.4	|- ( ph -> ( ps <-> ( ch /\ th /\ ta ) ) )
5	1 2 3	3jca	|- ( ph -> ( ch /\ th /\ ta ) )
6	5 4	mpbird	|- ( ph -> ps )