Theorem mpbiran2 941

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  2936  ss0b  3462  eusv1  4452  eusv2nf  4456  eusv2  4457  opthprc  4677  opelres  4912  f1cnvcnv  5432  fores  5447  f1orn  5471  funfvdm  5579  dfoprab2  5921  tpostpos  6264  opelreal  7825  elreal2  7828  eqresr  7834  axprecex  7878  zeoxor  11873  isprm2  12116  toptopon  13488  bdeq0  14589  subctctexmid  14720