Theorem mpbiran2 702

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 270	1 ⊢ (𝜑 ↔ 𝜓)

Syntax hints:   ↔ wb 198   ∧ wa 385

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 199  df-an 386

This theorem is referenced by:  pm5.62  1043  reueq  3600  ss0b  4167  eusv1  5059  eusv2nf  5063  eusv2  5064  opthprc  5368  sosn  5391  opelresOLD  5612  elridOLD  5668  fdmrn  6277  f1cnvcnv  6323  fores  6339  f1orn  6364  funfv  6488  dfoprab2  6933  elxp7  7434  tpostpos  7608  canthwe  9759  recmulnq  10072  opelreal  10237  elreal2  10239  eqresr  10244  elnn1uz2  12006  faclbnd4lem1  13329  isprm2  15726  joindm  17315  meetdm  17329  symgbas0  18123  efgs1  18458  toptopon  21047  ist1-3  21479  perfcls  21495  prdsxmetlem  22498  rusgrprc  26832  hhsssh2  28644  choc0  28702  chocnul  28704  shlesb1i  28762  adjeu  29265  isarchi  30244  derang0  31660  dfon3  32504  brtxpsd  32506  topmeet  32863  filnetlem2  32878  filnetlem3  32879  bj-rabtrALT  33413  bj-snsetex  33435  relowlpssretop  33702  poimirlem28  33918  fdc  34020  0totbnd  34051  heiborlem3  34091  cossssid  34703  cnvrefrelcoss2  34769  ifpid3g  38609  elintima  38716