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  2451  velcomp  4057  0pss  4363  pssv  4365  disj4  4415  pwpwab  5066  zfpair  5387  opabn0  5532  relop  5834  ssrnres  6182  funopab  6595  funcnv2  6630  fnres  6688  dffv2  7003  funcnvmpt  7018  idref  7173  rnoprab  7548  suppssr  8240  frrlem9  8340  brwitnlem  8543  omeu  8621  naddcllem  8713  elixp  8960  dfsup2  9463  card2inf  9576  harndom  9583  dford2  9648  cantnfp1lem3  9708  cantnfp1  9709  cantnflem1  9717  ttrclresv  9745  tz9.12lem3  9823  djulf1o  10020  djurf1o  10021  dfac4  10228  dfac12a  10254  cflem  10350  cfsmolem  10375  dffin7-2  10503  dfacfin7  10504  brdom3  10634  iunfo  10650  gch3  10788  lbfzo0  13861  fzo1lb  13875  1elfzo1  13876  gcdcllem3  16700  1nprm  16883  cygctb  20136  expmhm  21772  expghm  21811  opsrtoslem2  22395  mat1dimelbas  22816  basdif0  23301  txdis1cn  23984  trfil2  24236  txflf  24355  clsnsg  24459  tgpconncomp  24462  perfdvf  26253  wilthlem3  27427  noeta2  28177  sltssnb  28185  etaslts2  28210  made0  28279  bdayons  28692  noseqind  28708  zsoring  28825  mpteleeOLD  29503  iscplgr  30026  rgrprcx  30203  blocnilem  31436  h1de2i  32185  nmop0  32618  nmfn0  32619  lnopconi  32666  lnfnconi  32687  stcltr2i  32907  1stpreima  33371  2ndpreima  33372  suppss3  33385  rncardr1prc  35850  acwer1prc  35852  onvf1od  36035  vonf1oonfo  36049  fmla0  36314  fmlasuc0  36316  elmrsubrn  36452  dftr6  36694  br6  36700  dford5reg  36722  txpss3v  36818  brtxp  36820  brpprod  36825  brsset  36829  dfon3  36832  brtxpsd  36834  brtxpsd2  36835  dffun10  36854  elfuns  36855  funpartlem  36884  fullfunfv  36889  dfrdg4  36893  dfint3  36894  brub  36896  dffr7  36898  hfext  37112  neibastop2lem  37326  mh-inf3f1  37507  bj-equsexval  37737  bj-elid3  38280  finxp0  38506  finxp1o  38507  brvdif  39390  xrnss3v  39505  ntrneiel2  45278  ntrneik4w  45292  ismnushort  45477  permaxpow  46194  funressnvmo  48320  dfdfat2  48403  fucoisfunc  50692