Theorem mpbiran 721

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

Syntax hints:   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  mpbiran2  722  mpbir2an  723  pm5.63  1035  equsexALT  2449  velcomp  3919  0pss  4366  pssv  4368  disj4  4418  pwpwab  5068  zfpair  5392  opabn0  5538  relop  5836  ssrnres  6176  funopab  6571  funcnv2  6604  fnres  6662  dffv2  6976  funcnvmpt  6991  idref  7142  rnoprab  7515  suppssr  8190  frrlem9  8290  brwitnlem  8491  omeu  8569  naddcllem  8661  elixp  8901  dfsup2  9403  card2inf  9516  harndom  9523  dford2  9588  cantnfp1lem3  9648  cantnfp1  9649  cantnflem1  9657  ttrclresv  9685  tz9.12lem3  9760  djulf1o  9897  djurf1o  9898  dfac4  10105  dfac12a  10131  cflem  10227  cflemOLD  10228  cfsmolem  10253  dffin7-2  10381  dfacfin7  10382  brdom3  10511  iunfo  10522  gch3  10660  lbfzo0  13728  fzo1lb  13742  1elfzo1  13743  gcdcllem3  16558  1nprm  16736  cygctb  19961  expmhm  21565  expghm  21604  opsrtoslem2  22186  mat1dimelbas  22607  basdif0  23089  txdis1cn  23771  trfil2  24023  txflf  24142  clsnsg  24246  tgpconncomp  24249  perfdvf  26041  wilthlem3  27210  noeta2  27930  sltssnb  27938  etaslts2  27963  made0  28032  bdayons  28445  noseqind  28461  zsoring  28578  mpteleeOLD  29211  iscplgr  29731  rgrprcx  29908  blocnilem  31122  h1de2i  31871  nmop0  32304  nmfn0  32305  lnopconi  32352  lnfnconi  32373  stcltr2i  32593  1stpreima  33018  2ndpreima  33019  suppss3  33034  onvf1od  35557  vonf1oonfo  35565  fmla0  35840  fmlasuc0  35842  elmrsubrn  35978  dftr6  36209  br6  36215  dford5reg  36238  txpss3v  36334  brtxp  36336  brpprod  36341  brsset  36345  dfon3  36348  brtxpsd  36350  brtxpsd2  36351  dffun10  36370  elfuns  36371  funpartlem  36400  fullfunfv  36405  dfrdg4  36409  dfint3  36410  brub  36412  hfext  36641  neibastop2lem  36837  bj-equsexval  37248  bj-elid3  37777  finxp0  38003  finxp1o  38004  brvdif  38883  xrnss3v  38998  ntrneiel2  44782  ntrneik4w  44796  ismnushort  44981  permaxpow  45688  funressnvmo  47749  dfdfat2  47832