Theorem mpbiran2 950

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  3019  ss0b  3552  eusv1  4578  eusv2nf  4582  eusv2  4583  opthprc  4806  opelres  5048  f1cnvcnv  5589  fores  5605  f1orn  5629  funfvdm  5745  fdmrn  6007  dfoprab2  6108  tpostpos  6508  opelreal  8158  elreal2  8161  eqresr  8167  axprecex  8211  zeoxor  12580  isprm2  12839  toptopon  14995  bdeq0  16749  subctctexmid  16886