Theorem mpbiran2 723

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 468	. 2 ⊢ (𝜑 ↔ (𝜒 ∧ 𝜓))
4	1, 3	mpbiran 722	1 ⊢ (𝜑 ↔ 𝜓)

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

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 402

This theorem is used by:  pm5.62  1036  rabtru  3646  reueq  3698  ss0b  4354  eusv1  5360  eusv2nf  5364  eusv2  5365  dfid2  5556  opthprc  5723  sosn  5746  fdmrn  6738  f1cnvcnv  6786  fores  6803  f1orn  6832  funfv  6969  dfoprab2  7475  elxp7  8025  tpostpos  8248  frrlem11  8299  canthwe  10664  opelreal  11143  elreal2  11145  eqresr  11150  elnn1uz2  12978  faclbnd4lem1  14361  isprm2  16778  joindm  18467  meetdm  18481  symgbas0  19522  toptopon  23148  ist1-3  23580  perfcls  23596  prdsxmetlem  24600  eln0s  28634  rusgrprc  30058  hhsssh2  31759  choc0  31815  chocnul  31817  shlesb1i  31875  adjeu  32378  isarchi  33630  vonf1osev  35717  derang0  35756  dfon3  36477  brtxpsd  36479  topmeet  36991  filnetlem2  37006  filnetlem3  37007  bj-rabtrALT  37683  bj-snsetex  37715  bj-dfid2ALT  37817  relowlpssretop  38126  poimirlem28  38405  fdc  38503  0totbnd  38531  heiborlem3  38571  cossssid  39313  cnvrefrelcoss2  39373  dfdisjALTV  39554  dfeldisj2  39566  dfeldisj3  39567  dfeldisj4  39568  disjqmap2  39582  disjres  39600  disjxrn  39602  dfantisymrel4  39620  dfantisymrel5  39621  antisymrelres  39622  ifpid3g  44340  elintima  44501  brpermmodel  45834  0funcALT  50022