Theorem mpbiran2 906

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

Syntax hints:   ∧ wa 103   ↔ wb 104

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  reueq  2850  ss0b  3366  eusv1  4331  eusv2nf  4335  eusv2  4336  opthprc  4548  opelres  4780  f1cnvcnv  5295  fores  5310  f1orn  5331  funfvdm  5436  dfoprab2  5770  tpostpos  6113  opelreal  7556  elreal2  7559  eqresr  7565  axprecex  7609  zeoxor  11408  isprm2  11638  toptopon  12022  bdeq0  12748