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  2450  velcomp  3917  0pss  4363  pssv  4365  disj4  4415  pwpwab  5067  zfpair  5390  opabn0  5536  relop  5834  ssrnres  6175  funopab  6572  funcnv2  6605  fnres  6663  dffv2  6977  funcnvmpt  6992  idref  7146  rnoprab  7522  suppssr  8197  frrlem9  8297  brwitnlem  8498  omeu  8576  naddcllem  8668  elixp  8915  dfsup2  9418  card2inf  9531  harndom  9538  dford2  9603  cantnfp1lem3  9663  cantnfp1  9664  cantnflem1  9672  ttrclresv  9700  tz9.12lem3  9775  djulf1o  9921  djurf1o  9922  dfac4  10129  dfac12a  10155  cflem  10251  cfsmolem  10276  dffin7-2  10404  dfacfin7  10405  brdom3  10535  iunfo  10551  gch3  10689  lbfzo0  13759  fzo1lb  13773  1elfzo1  13774  gcdcllem3  16597  1nprm  16775  cygctb  20025  expmhm  21655  expghm  21694  opsrtoslem2  22278  mat1dimelbas  22699  basdif0  23184  txdis1cn  23867  trfil2  24119  txflf  24238  clsnsg  24342  tgpconncomp  24345  perfdvf  26137  wilthlem3  27314  noeta2  28034  sltssnb  28042  etaslts2  28067  made0  28136  bdayons  28549  noseqind  28565  zsoring  28682  mpteleeOLD  29360  iscplgr  29883  rgrprcx  30060  blocnilem  31293  h1de2i  32042  nmop0  32475  nmfn0  32476  lnopconi  32523  lnfnconi  32544  stcltr2i  32764  1stpreima  33187  2ndpreima  33188  suppss3  33202  onvf1od  35712  vonf1oonfo  35720  fmla0  35969  fmlasuc0  35971  elmrsubrn  36107  dftr6  36338  br6  36344  dford5reg  36367  txpss3v  36463  brtxp  36465  brpprod  36470  brsset  36474  dfon3  36477  brtxpsd  36479  brtxpsd2  36480  dffun10  36499  elfuns  36500  funpartlem  36529  fullfunfv  36534  dfrdg4  36538  dfint3  36539  brub  36541  dffr7  36543  hfext  36771  neibastop2lem  36987  bj-equsexval  37398  bj-elid3  37927  finxp0  38153  finxp1o  38154  brvdif  39022  xrnss3v  39137  ntrneiel2  44934  ntrneik4w  44948  ismnushort  45133  permaxpow  45840  funressnvmo  47941  dfdfat2  48024