Theorem mpbiran 717

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

Hypotheses

Ref	Expression
mpbiran.1	⊢ 𝜓
mpbiran.2	⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))

Assertion

Ref	Expression
mpbiran	⊢ (𝜑 ↔ 𝜒)

Proof of Theorem mpbiran

Step	Hyp	Ref	Expression
1		mpbiran.2	. 2 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))
2		mpbiran.1	. . 3 ⊢ 𝜓
3	2	biantrur 537	. 2 ⊢ (𝜒 ↔ (𝜓 ∧ 𝜒))
4	1, 3	bitr4i 280	1 ⊢ (𝜑 ↔ 𝜒)

Syntax hints:   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  mpbiran2  718  mpbir2an  719  pm5.63  1030  equsexALT  2444  velcomp  3914  0pss  4395  pssv  4397  disj4  4407  pwpwab  5054  zfpair  5372  opabn0  5517  relop  5815  ssrnres  6153  funopab  6545  funcnv2  6578  fnres  6637  dffv2  6951  funcnvmpt  6966  idref  7117  rnoprab  7490  suppssr  8163  frrlem9  8263  brwitnlem  8464  omeu  8542  naddcllem  8634  elixp  8875  dfsup2  9380  card2inf  9493  harndom  9500  dford2  9565  cantnfp1lem3  9625  cantnfp1  9626  cantnflem1  9634  ttrclresv  9662  tz9.12lem3  9737  djulf1o  9860  djurf1o  9861  dfac4  10068  dfac12a  10095  cflem  10191  cflemOLD  10192  cfsmolem  10217  dffin7-2  10345  dfacfin7  10346  brdom3  10475  iunfo  10486  gch3  10624  lbfzo0  13695  fzo1lb  13709  1elfzo1  13710  gcdcllem3  16511  1nprm  16689  cygctb  19908  expmhm  21461  expghm  21500  opsrtoslem2  22082  mat1dimelbas  22504  basdif0  22986  txdis1cn  23668  trfil2  23920  txflf  24039  clsnsg  24143  tgpconncomp  24146  perfdvf  25938  wilthlem3  27104  noeta2  27824  sltssnb  27832  etaslts2  27857  made0  27926  bdayons  28339  noseqind  28355  zsoring  28472  mpteleeOLD  29035  iscplgr  29555  rgrprcx  29732  blocnilem  30946  h1de2i  31695  nmop0  32128  nmfn0  32129  lnopconi  32176  lnfnconi  32197  stcltr2i  32417  1stpreima  32852  2ndpreima  32853  suppss3  32868  onvf1od  35405  fmla0  35680  fmlasuc0  35682  elmrsubrn  35818  dftr6  36049  br6  36055  dford5reg  36078  txpss3v  36174  brtxp  36176  brpprod  36181  brsset  36185  dfon3  36188  brtxpsd  36190  brtxpsd2  36191  dffun10  36210  elfuns  36211  funpartlem  36240  fullfunfv  36245  dfrdg4  36249  dfint3  36250  brub  36252  hfext  36481  neibastop2lem  36668  bj-equsexval  37080  bj-elid3  37607  finxp0  37833  finxp1o  37834  brvdif  38713  xrnss3v  38828  ntrneiel2  44610  ntrneik4w  44624  ismnushort  44825  permaxpow  45533  funressnvmo  47587  dfdfat2  47670