Theorem mpbi2and 945

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 )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  supisoti  7094  remim  11090  resqrtcl  11259  divalgmod  12157  oddpwdclemxy  12410  divnumden  12437  numdensq  12443  prmdivdiv  12478  4sqlem7  12626  ismgmid2  13130  mnd1  13205  iscmnd  13552  imasring  13744  subrg1  13911  topgele  14419  lmcn2  14670