Theorem mpbiran2 947

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

Hypotheses

Ref	Expression
mpbiran2.1	⊢ 𝜒
mpbiran2.2	⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))

Assertion

Ref	Expression
mpbiran2	⊢ (𝜑 ↔ 𝜓)

Proof of Theorem mpbiran2

Step	Hyp	Ref	Expression
1		mpbiran2.2	. 2 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))
2		mpbiran2.1	. . 3 ⊢ 𝜒
3	2	biantru 302	. 2 ⊢ (𝜓 ↔ (𝜓 ∧ 𝜒))
4	1, 3	bitr4i 187	1 ⊢ (𝜑 ↔ 𝜓)

Syntax hints:   ∧ wa 104   ↔ wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  reueq  3003  ss0b  3532  eusv1  4547  eusv2nf  4551  eusv2  4552  opthprc  4775  opelres  5016  f1cnvcnv  5550  fores  5566  f1orn  5590  funfvdm  5705  dfoprab2  6063  tpostpos  6425  opelreal  8040  elreal2  8043  eqresr  8049  axprecex  8093  zeoxor  12423  isprm2  12682  toptopon  14735  bdeq0  16412  subctctexmid  16551