Theorem mpbiran 722

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

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

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 402

This theorem is used by:  mpbiran2  723  mpbir2an  724  pm5.63  1037  equsexALT  2448  velcomp  3913  0pss  4359  pssv  4361  disj4  4411  pwpwab  5062  zfpair  5382  opabn0  5524  relop  5824  ssrnres  6165  funopab  6563  funcnv2  6596  fnres  6654  dffv2  6968  funcnvmpt  6983  idref  7137  rnoprab  7513  suppssr  8190  frrlem9  8290  brwitnlem  8493  omeu  8571  naddcllem  8663  elixp  8910  dfsup2  9414  card2inf  9527  harndom  9534  dford2  9599  cantnfp1lem3  9659  cantnfp1  9660  cantnflem1  9668  ttrclresv  9696  tz9.12lem3  9771  djulf1o  9965  djurf1o  9966  dfac4  10173  dfac12a  10199  cflem  10295  cfsmolem  10320  dffin7-2  10448  dfacfin7  10449  brdom3  10579  iunfo  10595  gch3  10733  lbfzo0  13803  fzo1lb  13817  1elfzo1  13818  gcdcllem3  16639  1nprm  16817  cygctb  20068  expmhm  21704  expghm  21743  opsrtoslem2  22327  mat1dimelbas  22748  basdif0  23233  txdis1cn  23916  trfil2  24168  txflf  24287  clsnsg  24391  tgpconncomp  24394  perfdvf  26185  wilthlem3  27361  noeta2  28081  sltssnb  28089  etaslts2  28114  made0  28183  bdayons  28596  noseqind  28612  zsoring  28729  mpteleeOLD  29407  iscplgr  29930  rgrprcx  30107  blocnilem  31340  h1de2i  32089  nmop0  32522  nmfn0  32523  lnopconi  32570  lnfnconi  32591  stcltr2i  32811  1stpreima  33234  2ndpreima  33235  suppss3  33249  onvf1od  35811  vonf1oonfo  35819  fmla0  36068  fmlasuc0  36070  elmrsubrn  36206  dftr6  36437  br6  36443  dford5reg  36466  txpss3v  36562  brtxp  36564  brpprod  36569  brsset  36573  dfon3  36576  brtxpsd  36578  brtxpsd2  36579  dffun10  36598  elfuns  36599  funpartlem  36628  fullfunfv  36633  dfrdg4  36637  dfint3  36638  brub  36640  dffr7  36642  hfext  36856  neibastop2lem  37070  mh-inf3f1  37251  bj-equsexval  37481  bj-elid3  38008  finxp0  38234  finxp1o  38235  brvdif  39118  xrnss3v  39233  ntrneiel2  45030  ntrneik4w  45044  ismnushort  45229  permaxpow  45936  funressnvmo  48037  dfdfat2  48120