Theorem mpbiran 706

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

Syntax hints:   ↔ wb 205   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  mpbiran2  707  mpbir2an  708  pm5.63  1017  equsexALT  2420  velcomp  3903  ddif  4072  dfun2  4194  dfin2  4195  0pss  4379  pssv  4381  disj4  4393  pwpwab  5033  zfpair  5345  opabn0  5467  relop  5762  ssrnres  6086  funopab  6476  funcnv2  6509  fnres  6568  dffv2  6872  idref  7027  rnoprab  7387  suppssr  8021  frrlem9  8119  brwitnlem  8346  omeu  8425  elixp  8701  1sdom  9034  dfsup2  9212  card2inf  9323  harndom  9330  dford2  9387  cantnfp1lem3  9447  cantnfp1  9448  cantnflem1  9456  ttrclresv  9484  tz9.12lem3  9556  djulf1o  9679  djurf1o  9680  dfac4  9887  dfac12a  9913  cflem  10011  cfsmolem  10035  dffin7-2  10163  dfacfin7  10164  brdom3  10293  iunfo  10304  gch3  10441  lbfzo0  13436  gcdcllem3  16217  1nprm  16393  cygctb  19502  expmhm  20676  expghm  20706  opsrtoslem2  21272  mat1dimelbas  21629  basdif0  22112  txdis1cn  22795  trfil2  23047  txflf  23166  clsnsg  23270  tgpconncomp  23273  perfdvf  25076  wilthlem3  26228  mptelee  27272  iscplgr  27791  rgrprcx  27968  blocnilem  29175  h1de2i  29924  nmop0  30357  nmfn0  30358  lnopconi  30405  lnfnconi  30426  stcltr2i  30646  funcnvmpt  31013  1stpreima  31048  2ndpreima  31049  suppss3  31068  fmla0  33353  fmlasuc0  33355  elmrsubrn  33491  dftr6  33727  br6  33733  dford5reg  33767  naddcllem  33840  noeta2  33988  etasslt2  34017  made0  34066  txpss3v  34189  brtxp  34191  brpprod  34196  brsset  34200  dfon3  34203  brtxpsd  34205  brtxpsd2  34206  dffun10  34225  elfuns  34226  funpartlem  34253  fullfunfv  34258  dfrdg4  34262  dfint3  34263  brub  34265  hfext  34494  neibastop2lem  34558  bj-equsexval  34850  bj-elid3  35347  finxp0  35571  finxp1o  35572  brvdif  36408  xrnss3v  36509  ntrneiel2  41703  ntrneik4w  41717  ismnushort  41926  funressnvmo  44550  dfdfat2  44631