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 ⊢ (𝜑 ↔ 𝜒)

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 400

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 401

This theorem is used by:  mpbiran2  722  mpbir2an  723  pm5.63  1036  equsexALT  2450  velcomp  3919  0pss  4366  pssv  4368  disj4  4418  pwpwab  5068  zfpair  5391  opabn0  5537  relop  5835  ssrnres  6175  funopab  6571  funcnv2  6604  fnres  6662  dffv2  6976  funcnvmpt  6991  idref  7142  rnoprab  7517  suppssr  8189  frrlem9  8289  brwitnlem  8490  omeu  8568  naddcllem  8660  elixp  8900  dfsup2  9402  card2inf  9515  harndom  9522  dford2  9587  cantnfp1lem3  9647  cantnfp1  9648  cantnflem1  9656  ttrclresv  9684  tz9.12lem3  9759  djulf1o  9905  djurf1o  9906  dfac4  10113  dfac12a  10139  cflem  10235  cfsmolem  10260  dffin7-2  10388  dfacfin7  10389  brdom3  10518  iunfo  10529  gch3  10667  lbfzo0  13735  fzo1lb  13749  1elfzo1  13750  gcdcllem3  16565  1nprm  16743  cygctb  19968  expmhm  21597  expghm  21636  opsrtoslem2  22218  mat1dimelbas  22639  basdif0  23121  txdis1cn  23803  trfil2  24055  txflf  24174  clsnsg  24278  tgpconncomp  24281  perfdvf  26073  wilthlem3  27245  noeta2  27965  sltssnb  27973  etaslts2  27998  made0  28067  bdayons  28480  noseqind  28496  zsoring  28613  mpteleeOLD  29256  iscplgr  29776  rgrprcx  29953  blocnilem  31167  h1de2i  31916  nmop0  32349  nmfn0  32350  lnopconi  32397  lnfnconi  32418  stcltr2i  32638  1stpreima  33063  2ndpreima  33064  suppss3  33079  onvf1od  35599  vonf1oonfo  35607  fmla0  35882  fmlasuc0  35884  elmrsubrn  36020  dftr6  36251  br6  36257  dford5reg  36280  txpss3v  36376  brtxp  36378  brpprod  36383  brsset  36387  dfon3  36390  brtxpsd  36392  brtxpsd2  36393  dffun10  36412  elfuns  36413  funpartlem  36442  fullfunfv  36447  dfrdg4  36451  dfint3  36452  brub  36454  hfext  36683  neibastop2lem  36899  bj-equsexval  37310  bj-elid3  37839  finxp0  38065  finxp1o  38066  brvdif  38943  xrnss3v  39058  ntrneiel2  44840  ntrneik4w  44854  ismnushort  45039  permaxpow  45746  funressnvmo  47810  dfdfat2  47893