Theorem mpbiran 708

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

Syntax hints:   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  mpbiran2  709  mpbir2an  710  pm5.63  1020  equsexALT  2427  velcomp  3991  ddif  4164  dfun2  4289  dfin2  4290  0pss  4470  pssv  4472  disj4  4482  pwpwab  5126  zfpair  5439  opabn0  5572  relop  5875  ssrnres  6209  funopab  6613  funcnv2  6646  fnres  6707  dffv2  7017  idref  7180  rnoprab  7554  suppssr  8236  frrlem9  8335  brwitnlem  8563  omeu  8641  naddcllem  8732  elixp  8962  1sdomOLD  9312  dfsup2  9513  card2inf  9624  harndom  9631  dford2  9689  cantnfp1lem3  9749  cantnfp1  9750  cantnflem1  9758  ttrclresv  9786  tz9.12lem3  9858  djulf1o  9981  djurf1o  9982  dfac4  10191  dfac12a  10218  cflem  10314  cflemOLD  10315  cfsmolem  10339  dffin7-2  10467  dfacfin7  10468  brdom3  10597  iunfo  10608  gch3  10745  lbfzo0  13756  gcdcllem3  16547  1nprm  16726  cygctb  19934  expmhm  21477  expghm  21509  opsrtoslem2  22103  mat1dimelbas  22498  basdif0  22981  txdis1cn  23664  trfil2  23916  txflf  24035  clsnsg  24139  tgpconncomp  24142  perfdvf  25958  wilthlem3  27131  noeta2  27847  etasslt2  27877  made0  27930  noseqind  28316  mptelee  28928  iscplgr  29450  rgrprcx  29628  blocnilem  30836  h1de2i  31585  nmop0  32018  nmfn0  32019  lnopconi  32066  lnfnconi  32087  stcltr2i  32307  funcnvmpt  32685  1stpreima  32718  2ndpreima  32719  suppss3  32738  fmla0  35350  fmlasuc0  35352  elmrsubrn  35488  dftr6  35713  br6  35719  dford5reg  35746  txpss3v  35842  brtxp  35844  brpprod  35849  brsset  35853  dfon3  35856  brtxpsd  35858  brtxpsd2  35859  dffun10  35878  elfuns  35879  funpartlem  35906  fullfunfv  35911  dfrdg4  35915  dfint3  35916  brub  35918  hfext  36147  neibastop2lem  36326  bj-equsexval  36626  bj-elid3  37133  finxp0  37357  finxp1o  37358  brvdif  38217  xrnss3v  38328  ntrneiel2  44048  ntrneik4w  44062  ismnushort  44270  funressnvmo  46960  dfdfat2  47043