Theorem mpbiran2 954

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

This proof depends on syntax axioms:   /\ wa 104   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  reueq  3025  ss0b  3562  eusv1  4598  eusv2nf  4602  eusv2  4603  opthprc  4826  opelres  5068  f1cnvcnv  5609  fores  5625  f1orn  5649  funfvdm  5766  fdmrn  6034  dfoprab2  6135  tpostpos  6535  opelreal  8194  elreal2  8197  eqresr  8203  axprecex  8247  zeoxor  12636  isprm2  12895  toptopon  15119  bdeq0  16893  subctctexmid  17030