Theorem mpbiran 709

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

Syntax hints:   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  mpbiran2  710  mpbir2an  711  pm5.63  1021  equsexALT  2417  velcomp  3920  ddif  4094  dfun2  4223  dfin2  4224  0pss  4400  pssv  4402  disj4  4412  pwpwab  5055  zfpair  5363  opabn0  5500  relop  5797  ssrnres  6131  funopab  6521  funcnv2  6554  fnres  6613  dffv2  6922  idref  7084  rnoprab  7458  suppssr  8135  frrlem9  8234  brwitnlem  8432  omeu  8510  naddcllem  8601  elixp  8838  dfsup2  9353  card2inf  9466  harndom  9473  dford2  9535  cantnfp1lem3  9595  cantnfp1  9596  cantnflem1  9604  ttrclresv  9632  tz9.12lem3  9704  djulf1o  9827  djurf1o  9828  dfac4  10035  dfac12a  10062  cflem  10158  cflemOLD  10159  cfsmolem  10183  dffin7-2  10311  dfacfin7  10312  brdom3  10441  iunfo  10452  gch3  10589  lbfzo0  13620  fzo1lb  13634  1elfzo1  13635  gcdcllem3  16430  1nprm  16608  cygctb  19789  expmhm  21361  expghm  21400  opsrtoslem2  21979  mat1dimelbas  22374  basdif0  22856  txdis1cn  23538  trfil2  23790  txflf  23909  clsnsg  24013  tgpconncomp  24016  perfdvf  25820  wilthlem3  26996  noeta2  27713  etasslt2  27743  made0  27805  bdayon  28196  noseqind  28209  zsoring  28319  mptelee  28858  iscplgr  29378  rgrprcx  29556  blocnilem  30766  h1de2i  31515  nmop0  31948  nmfn0  31949  lnopconi  31996  lnfnconi  32017  stcltr2i  32237  funcnvmpt  32624  1stpreima  32663  2ndpreima  32664  suppss3  32680  onvf1od  35079  fmla0  35354  fmlasuc0  35356  elmrsubrn  35492  dftr6  35723  br6  35729  dford5reg  35755  txpss3v  35851  brtxp  35853  brpprod  35858  brsset  35862  dfon3  35865  brtxpsd  35867  brtxpsd2  35868  dffun10  35887  elfuns  35888  funpartlem  35915  fullfunfv  35920  dfrdg4  35924  dfint3  35925  brub  35927  hfext  36156  neibastop2lem  36333  bj-equsexval  36633  bj-elid3  37140  finxp0  37364  finxp1o  37365  brvdif  38235  xrnss3v  38339  ntrneiel2  44059  ntrneik4w  44073  ismnushort  44274  permaxpow  44983  funressnvmo  47030  dfdfat2  47113