Theorem mpbiranr 548

Description: Detach truth from conjunction in biconditional.

Hypotheses

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

Assertion

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

Proof of Theorem mpbiranr

Step	Hyp	Ref	Expression
1		mpbiranr.1	. 2 |- (ph <-> (ps /\ ch))
2		mpbiranr.2	. . 3 |- ch
3	2	biantru 543	. 2 |- (ps <-> (ps /\ ch))
4	1, 3	bitr4 154	1 |- (ph <-> ps)

Syntax hints:   <-> wb 127   /\ wa 196

This theorem is referenced by:  pw0 1882  opthprc 2457  opelres 2579  funex 2741  f1cnv 2782  fores 2794  funfvop 2857  funfv 2862  iinon 2948  recmulpq 3864  genpdm 3899  genpn0 3900  opelreal 4043  eqresr 4049  axicn 4065  chocnul 5293  shlesb1 5360

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

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org