Theorem mpbiran2 953

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

Syntax hints:   ↔ wb 196   ∧ wa 384

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 386

This theorem is referenced by:  pm5.62  957  reueq  3386  ss0b  3945  eusv1  4820  eusv2nf  4824  eusv2  4825  opthprc  5127  sosn  5149  opelres  5361  fdmrn  6021  f1cnvcnv  6066  fores  6081  f1orn  6104  funfv  6222  dfoprab2  6654  elxp7  7146  tpostpos  7317  canthwe  9417  recmulnq  9730  opelreal  9895  elreal2  9897  eqresr  9902  elnn1uz2  11709  faclbnd4lem1  13020  isprm2  15319  joindm  16924  meetdm  16938  symgbas0  17735  efgs1  18069  toptopon  20648  ist1-3  21063  perfcls  21079  prdsxmetlem  22083  rusgrprc  26356  hhsssh2  27973  choc0  28031  chocnul  28033  shlesb1i  28091  adjeu  28594  isarchi  29518  derang0  30856  brtxp  31626  brpprod  31631  dfon3  31638  brtxpsd  31640  topmeet  31998  filnetlem2  32013  filnetlem3  32014  bj-rabtrALT  32571  bj-snsetex  32595  relowlpssretop  32841  poimirlem28  33066  fdc  33170  0totbnd  33201  heiborlem3  33241  ifpid3g  37315  elintima  37423