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  3002  ss0b  3531  eusv1  4543  eusv2nf  4547  eusv2  4548  opthprc  4770  opelres  5010  f1cnvcnv  5544  fores  5560  f1orn  5584  funfvdm  5699  dfoprab2  6057  tpostpos  6416  opelreal  8022  elreal2  8025  eqresr  8031  axprecex  8075  zeoxor  12388  isprm2  12647  toptopon  14700  bdeq0  16254  subctctexmid  16395