Theorem mpbiran 798

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 794	. 2 |- (ch <-> (ps /\ ch))
4	1, 3	bitr4i 193	1 |- (ph <-> ch)

Syntax hints:   <-> wb 163   /\ wa 240

This theorem is referenced by:  mpbir2an 800  elabs 2489  ddif 2737  dfun2 2829  dfin2 2830  0pss 2910  pssv 2913  disj4 2922  zfpair 3522  opabn0 3575  so0OLD 3622  relop 4113  funopab 4455  dff12 4609  dffv2 4734  eqfnfv2OLD 4768  rnoprab 4933  0sdomg 5529  aceq4 5896  brdom3 5963  cflem 6053  genpass 6264  elreal 6402  dfuzi 7414  ivthlem7 8549  pjthlem14 10865  h1de2i 11109  lnopconi 11600  lnfnconi 11627  stcltr2i 11847  divalglem2 13698  gcdcllem3 13720  algrf 13739  1nprm 13769  dftr6 13834  dford3 13848  txpss3v 14065  brsset 14069  dfon3 14072  brbigcup 14074  rcfpfillem3 14930

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 164  df-an 242

Copyright terms: Public domain