Theorem mpbiran2 974

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

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

Syntax hints:   ↔ wb 196   ∧ wa 383

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 197  df-an 385

This theorem is referenced by:  pm5.62  978  reueq  3437  ss0b  4006  eusv1  4890  eusv2nf  4894  eusv2  4895  opthprc  5201  sosn  5222  opelresOLD  5438  fdmrn  6102  f1cnvcnv  6147  fores  6162  f1orn  6185  funfv  6304  dfoprab2  6743  elxp7  7245  tpostpos  7417  canthwe  9511  recmulnq  9824  opelreal  9989  elreal2  9991  eqresr  9996  elnn1uz2  11803  faclbnd4lem1  13120  isprm2  15442  joindm  17050  meetdm  17064  symgbas0  17860  efgs1  18194  toptopon  20770  ist1-3  21201  perfcls  21217  prdsxmetlem  22220  rusgrprc  26542  hhsssh2  28255  choc0  28313  chocnul  28315  shlesb1i  28373  adjeu  28876  isarchi  29864  derang0  31277  brtxp  32112  brpprod  32117  dfon3  32124  brtxpsd  32126  topmeet  32484  filnetlem2  32499  filnetlem3  32500  bj-rabtrALT  33052  bj-snsetex  33076  relowlpssretop  33342  poimirlem28  33567  fdc  33671  0totbnd  33702  heiborlem3  33742  cossssid  34357  cnvrefrelcoss2  34423  ifpid3g  38154  elintima  38262