Theorem mpbi2and 956

Description: Detach a conjunction of truths in a biconditional. (Contributed by NM, 6-Nov-2011.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)

Hypotheses

Ref	Expression
mpbi2and.1	|- ( ph -> ps )
mpbi2and.2	|- ( ph -> ch )
mpbi2and.3	|- ( ph -> ( ( ps /\ ch ) <-> th ) )

Assertion

Ref	Expression
mpbi2and	|- ( ph -> th )

Proof of Theorem mpbi2and

Step	Hyp	Ref	Expression
1		mpbi2and.1	. . 3 |- ( ph -> ps )
2		mpbi2and.2	. . 3 |- ( ph -> ch )
3	1, 2	jca 306	. 2 |- ( ph -> ( ps /\ ch ) )
4		mpbi2and.3	. 2 |- ( ph -> ( ( ps /\ ch ) <-> th ) )
5	3, 4	mpbid 147	1 |- ( ph -> th )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  supisoti  7350  remim  11625  resqrtcl  11795  divalgmod  12694  oddpwdclemxy  12947  divnumden  12974  numdensq  12980  prmdivdiv  13015  4sqlem7  13163  ismgmid2  13700  mnd1  13762  iscmnd  14101  imasring  14369  subrg1  14539  topgele  15130  lmcn2  15381