Theorem mpbiran2 799

Description: Detach truth from conjunction in biconditional.

Hypotheses

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

Assertion

Ref	Expression
mpbiran2	|- (ph <-> ps)

Proof of Theorem mpbiran2

Step	Hyp	Ref	Expression
1		mpbiran.1	. 2 |- (ph <-> (ps /\ ch))
2		mpbiran2.2	. . 3 |- ch
3	2	biantru 793	. 2 |- (ps <-> (ps /\ ch))
4	1, 3	bitr4i 193	1 |- (ph <-> ps)

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

This theorem is referenced by:  pm5.62 805  ss0b 2901  eualeq 3823  euexeqOLD 3826  opthprc 4046  opelres 4222  f1cnv 4611  fores 4627  funbrfvb 4714  funfv 4731  elxp7 5042  iinon 5115  recmulpq 6222  genpdm 6257  genpn0 6258  opelreal 6401  eqresr 6407  faclbnd4lem1 8200  isummulc1 8473  hhsssh2 10773  chocnul 10925  shlesb1i 10992  divalglem2 13698  axfelem8 14038  dfon3 14072  brbigcup 14074  cmpdom 14481  fdc 15812  pleval2 16785

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