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  7351  remim  11641  resqrtcl  11811  divalgmod  12713  nnmaxpwlemxy  12967  divnumden  12995  numdensq  13001  prmdivdiv  13038  4sqlem7  13186  ismgmid2  13753  mnd1  13815  resscntz  14160  iscmnd  14185  imasring  14453  subrg1  14623  topgele  15221  lmcn2  15472