Theorem mpbiran2 925

Description: Detach truth from conjunction in biconditional. (Contributed by NM, 22-Feb-1996.) (Revised by NM, 9-Jan-2015.)

Hypotheses

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

Assertion

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

Proof of Theorem mpbiran2

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

Syntax hints:   /\ wa 103   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  reueq  2878  ss0b  3397  eusv1  4368  eusv2nf  4372  eusv2  4373  opthprc  4585  opelres  4819  f1cnvcnv  5334  fores  5349  f1orn  5370  funfvdm  5477  dfoprab2  5811  tpostpos  6154  opelreal  7628  elreal2  7631  eqresr  7637  axprecex  7681  zeoxor  11555  isprm2  11787  toptopon  12174  bdeq0  13054  subctctexmid  13185