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  2453  velcomp  3922  0pss  4404  pssv  4406  disj4  4416  pwpwab  5065  zfpair  5383  opabn0  5529  relop  5827  ssrnres  6168  funopab  6560  funcnv2  6593  fnres  6652  dffv2  6966  funcnvmpt  6981  idref  7132  rnoprab  7505  suppssr  8179  frrlem9  8279  brwitnlem  8480  omeu  8558  naddcllem  8650  elixp  8890  dfsup2  9392  card2inf  9505  harndom  9512  dford2  9577  cantnfp1lem3  9637  cantnfp1  9638  cantnflem1  9646  ttrclresv  9674  tz9.12lem3  9749  djulf1o  9886  djurf1o  9887  dfac4  10094  dfac12a  10120  cflem  10216  cflemOLD  10217  cfsmolem  10242  dffin7-2  10370  dfacfin7  10371  brdom3  10500  iunfo  10511  gch3  10649  lbfzo0  13719  fzo1lb  13733  1elfzo1  13734  gcdcllem3  16549  1nprm  16727  cygctb  19953  expmhm  21546  expghm  21585  opsrtoslem2  22167  mat1dimelbas  22589  basdif0  23071  txdis1cn  23753  trfil2  24005  txflf  24124  clsnsg  24228  tgpconncomp  24231  perfdvf  26023  wilthlem3  27192  noeta2  27912  sltssnb  27920  etaslts2  27945  made0  28014  bdayons  28427  noseqind  28443  zsoring  28560  mpteleeOLD  29154  iscplgr  29674  rgrprcx  29851  blocnilem  31065  h1de2i  31814  nmop0  32247  nmfn0  32248  lnopconi  32295  lnfnconi  32316  stcltr2i  32536  1stpreima  32964  2ndpreima  32965  suppss3  32980  onvf1od  35462  vonf1oonfo  35470  fmla0  35745  fmlasuc0  35747  elmrsubrn  35883  dftr6  36114  br6  36120  dford5reg  36143  txpss3v  36239  brtxp  36241  brpprod  36246  brsset  36250  dfon3  36253  brtxpsd  36255  brtxpsd2  36256  dffun10  36275  elfuns  36276  funpartlem  36305  fullfunfv  36310  dfrdg4  36314  dfint3  36315  brub  36317  hfext  36546  neibastop2lem  36733  bj-equsexval  37144  bj-elid3  37671  finxp0  37897  finxp1o  37898  brvdif  38777  xrnss3v  38892  ntrneiel2  44674  ntrneik4w  44688  ismnushort  44875  permaxpow  45583  funressnvmo  47637  dfdfat2  47720