Theorem mpbiran2 722

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.1	. 2 ⊢ 𝜒
2		mpbiran2.2	. . 3 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))
3	2	biancomi 467	. 2 ⊢ (𝜑 ↔ (𝜒 ∧ 𝜓))
4	1, 3	mpbiran 721	1 ⊢ (𝜑 ↔ 𝜓)

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 400

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 401

This theorem is used by:  pm5.62  1035  rabtru  3647  reueq  3699  ss0b  4357  eusv1  5361  eusv2nf  5365  eusv2  5366  dfid2  5557  opthprc  5724  sosn  5747  fdmrn  6737  f1cnvcnv  6785  fores  6802  f1orn  6831  funfv  6968  dfoprab2  7470  elxp7  8019  tpostpos  8240  frrlem11  8291  canthwe  10642  opelreal  11121  elreal2  11123  eqresr  11128  elnn1uz2  12955  faclbnd4lem1  14336  isprm2  16746  joindm  18435  meetdm  18449  symgbas0  19465  toptopon  23085  ist1-3  23517  perfcls  23533  prdsxmetlem  24536  eln0s  28565  rusgrprc  29951  hhsssh2  31633  choc0  31689  chocnul  31691  shlesb1i  31749  adjeu  32252  isarchi  33511  vonf1osev  35604  derang0  35669  dfon3  36390  brtxpsd  36392  topmeet  36903  filnetlem2  36918  filnetlem3  36919  bj-rabtrALT  37595  bj-snsetex  37627  bj-dfid2ALT  37729  relowlpssretop  38038  poimirlem28  38327  fdc  38424  0totbnd  38452  heiborlem3  38492  cossssid  39234  cnvrefrelcoss2  39294  dfdisjALTV  39475  dfeldisj2  39487  dfeldisj3  39488  dfeldisj4  39489  disjqmap2  39503  disjres  39521  disjxrn  39523  dfantisymrel4  39541  dfantisymrel5  39542  antisymrelres  39543  ifpid3g  44246  elintima  44407  brpermmodel  45740  0funcALT  49894