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  11639  resqrtcl  11809  divalgmod  12710  nnmaxpwlemxy  12964  divnumden  12992  numdensq  12998  prmdivdiv  13035  4sqlem7  13183  ismgmid2  13749  mnd1  13811  iscmnd  14150  imasring  14418  subrg1  14588  topgele  15179  lmcn2  15430