Theorem mpbiran 884

Description: Detach truth from conjunction in biconditional. (Contributed by NM, 27-Feb-1996.)

Hypotheses

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

Assertion

Ref	Expression
mpbiran	⊢ (φ ↔ χ)

Proof of Theorem mpbiran

Step	Hyp	Ref	Expression
1		mpbiran.2	. 2 ⊢ (φ ↔ (ψ ∧ χ))
2		mpbiran.1	. . 3 ⊢ ψ
3	2	biantrur 492	. 2 ⊢ (χ ↔ (ψ ∧ χ))
4	1, 3	bitr4i 243	1 ⊢ (φ ↔ χ)

Syntax hints:   ↔ wb 176   ∧ wa 358

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

This theorem depends on definitions:  df-bi 177  df-an 360

This theorem is referenced by:  mpbir2an  886  pm5.63  890  ddif  3398  dfun2  3490  dfin2  3491  0pss  3588  pssv  3590  disj4  3599  cnvkexg  4286  ssetkex  4294  sikexg  4296  ins2kexg  4305  ins3kexg  4306  nnsucelrlem1  4424  ncfinlowerlem1  4482  eqtfinrelk  4486  evenfinex  4503  oddfinex  4504  opabn0  4716  setconslem6  4736  fnres  5199  dmsi  5519  otelins2  5791  composeex  5820  dmpprod  5840  crossex  5850  transex  5910  enmap2  6068  csucex  6259  nmembers1lem1  6268  nchoicelem18  6306  dmfrec  6316  fnfreclem1  6317