Theorem mpbiran 727

Description: Detach truth from conjunction in biconditional.

Hypotheses

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

Assertion

Ref	Expression
mpbiran	|- (ph <-> ch)

Proof of Theorem mpbiran

Step	Hyp	Ref	Expression
1		mpbiran.1	. 2 |- (ph <-> (ps /\ ch))
2		mpbiran.2	. . 3 |- ps
3	2	biantrur 724	. 2 |- (ch <-> (ps /\ ch))
4	1, 3	bitr4 176	1 |- (ph <-> ch)

Syntax hints:   <-> wb 146   /\ wa 223

This theorem is referenced by:  mpbir2an 729  elabs 1962  ddif 2165  dfun2 2239  dfin2 2240  0pss 2304  pssv 2306  disj4 2313  zfpair 2772  opabn0 2819  so0 2860  relop 3270  funopab 3540  f11 3655  rnoprab 3995  0sdomg 4452  aceq4 4714  brdom3 4781  cflem 4885  genpass 5092  elreal 5230  dfuz 6158  ivthlem7 7230  ivthlem7OLD 7239  pjthlem14 9170  h1de2 9414  ho01 9694  lnopcon 9901  lnfncon 9928  pjinvar 10057  stcltr2 10140

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain