Theorem mpbiran2 882

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 296	. 2 ⊢ (𝜓 ↔ (𝜓 ∧ 𝜒))
4	1, 3	bitr4i 185	1 ⊢ (𝜑 ↔ 𝜓)

Syntax hints:   ∧ wa 102   ↔ wb 103

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  reueq  2789  ss0b  3283  eusv1  4202  eusv2nf  4206  eusv2  4207  opthprc  4409  opelres  4635  f1cnvcnv  5120  fores  5135  f1orn  5156  funfvdm  5257  dfoprab2  5572  tpostpos  5902  opelreal  6996  elreal2  6999  eqresr  7004  axprecex  7046  zeoxor  10268  isprm2  10499  bdeq0  10658