Theorem mpbiran 728

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 725	. 2 |- (ch <-> (ps /\ ch))
4	1, 3	bitr4 176	1 |- (ph <-> ch)

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

This theorem is referenced by:  mpbir2an 730  elabs 1966  ddif 2169  dfun2 2243  dfin2 2244  0pss 2308  pssv 2310  disj4 2317  zfpair 2777  opabn0 2824  so0 2865  relop 3275  funopab 3548  f11 3664  rnoprab 4004  0sdomg 4466  aceq4 4734  brdom3 4801  cflem 4905  genpass 5112  elreal 5250  dfuz 6202  ivthlem7 7287  pjthlem14 9232  h1de2 9476  ho01 9754  lnopcon 9963  lnfncon 9990  pjinvar 10119  stcltr2 10202  rcfpfillem3 10589  rcfpfillem3OLD 10590

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