Theorem mpbiran 709

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  710  mpbir2an  711  pm5.63  1021  equsexALT  2423  velcomp  3941  ddif  4116  dfun2  4245  dfin2  4246  0pss  4422  pssv  4424  disj4  4434  pwpwab  5079  zfpair  5391  opabn0  5528  relop  5830  ssrnres  6167  funopab  6570  funcnv2  6603  fnres  6664  dffv2  6973  idref  7135  rnoprab  7510  suppssr  8192  frrlem9  8291  brwitnlem  8517  omeu  8595  naddcllem  8686  elixp  8916  1sdomOLD  9255  dfsup2  9454  card2inf  9567  harndom  9574  dford2  9632  cantnfp1lem3  9692  cantnfp1  9693  cantnflem1  9701  ttrclresv  9729  tz9.12lem3  9801  djulf1o  9924  djurf1o  9925  dfac4  10134  dfac12a  10161  cflem  10257  cflemOLD  10258  cfsmolem  10282  dffin7-2  10410  dfacfin7  10411  brdom3  10540  iunfo  10551  gch3  10688  lbfzo0  13714  fzo1lb  13728  gcdcllem3  16518  1nprm  16696  cygctb  19871  expmhm  21402  expghm  21434  opsrtoslem2  22012  mat1dimelbas  22407  basdif0  22889  txdis1cn  23571  trfil2  23823  txflf  23942  clsnsg  24046  tgpconncomp  24049  perfdvf  25854  wilthlem3  27030  noeta2  27746  etasslt2  27776  made0  27829  noseqind  28215  mptelee  28820  iscplgr  29340  rgrprcx  29518  blocnilem  30731  h1de2i  31480  nmop0  31913  nmfn0  31914  lnopconi  31961  lnfnconi  31982  stcltr2i  32202  funcnvmpt  32591  1stpreima  32630  2ndpreima  32631  suppss3  32647  fmla0  35350  fmlasuc0  35352  elmrsubrn  35488  dftr6  35714  br6  35720  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  36324  bj-equsexval  36624  bj-elid3  37131  finxp0  37355  finxp1o  37356  brvdif  38225  xrnss3v  38336  ntrneiel2  44057  ntrneik4w  44071  ismnushort  44273  permaxpow  44982  funressnvmo  47022  dfdfat2  47105