Theorem mpbiran 547

Description: Detach truth from conjunction in biconditional.

Hypotheses

Ref	Expression
mpbiran.1	⊢ (φ ↔ (ψ ∧ χ))
mpbiran.2	⊢ ψ

Assertion

Ref	Expression
mpbiran	⊢ (φ ↔ χ)

Proof of Theorem mpbiran

Step	Hyp	Ref	Expression
1		mpbiran.1	. 2 ⊢ (φ ↔ (ψ ∧ χ))
2		mpbiran.2	. . 3 ⊢ ψ
3	2	biantrur 544	. 2 ⊢ (χ ↔ (ψ ∧ χ))
4	1, 3	bitr4 154	1 ⊢ (φ ↔ χ)

Syntax hints:   ↔ wb 127   ∧ wa 196

This theorem is referenced by:  elabs 1458  ddif 1597  dfun2 1668  dfin2 1669  0pss 1730  pssv 1732  disj4 1737  zfpair 1891  so0 2153  funopab 2694  f11 2780  rnoprab 3033  oawordeulem 3156  0sdom 3368  aceq4 3557  cflem 3700  genpass 3906  elreal 4044  pjthlem14 5238  h1de2 5458  hoeq 5595  stcltr2 5708

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org