Theorem mpbiran 708

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 205   ∧ 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 206  df-an 396

This theorem is referenced by:  mpbiran2  709  mpbir2an  710  pm5.63  1018  equsexALT  2414  velcomp  3962  ddif  4135  dfun2  4260  dfin2  4261  0pss  4445  pssv  4447  disj4  4459  pwpwab  5106  zfpair  5421  opabn0  5555  relop  5853  ssrnres  6182  funopab  6588  funcnv2  6621  fnres  6682  dffv2  6993  idref  7155  rnoprab  7524  suppssr  8201  frrlem9  8300  brwitnlem  8528  omeu  8606  naddcllem  8697  elixp  8923  1sdomOLD  9274  dfsup2  9468  card2inf  9579  harndom  9586  dford2  9644  cantnfp1lem3  9704  cantnfp1  9705  cantnflem1  9713  ttrclresv  9741  tz9.12lem3  9813  djulf1o  9936  djurf1o  9937  dfac4  10146  dfac12a  10172  cflem  10270  cfsmolem  10294  dffin7-2  10422  dfacfin7  10423  brdom3  10552  iunfo  10563  gch3  10700  lbfzo0  13705  gcdcllem3  16476  1nprm  16650  cygctb  19847  expmhm  21369  expghm  21401  opsrtoslem2  22000  mat1dimelbas  22386  basdif0  22869  txdis1cn  23552  trfil2  23804  txflf  23923  clsnsg  24027  tgpconncomp  24030  perfdvf  25845  wilthlem3  27015  noeta2  27730  etasslt2  27760  made0  27813  noseqind  28178  mptelee  28719  iscplgr  29241  rgrprcx  29419  blocnilem  30627  h1de2i  31376  nmop0  31809  nmfn0  31810  lnopconi  31857  lnfnconi  31878  stcltr2i  32098  funcnvmpt  32466  1stpreima  32499  2ndpreima  32500  suppss3  32519  fmla0  34992  fmlasuc0  34994  elmrsubrn  35130  dftr6  35345  br6  35351  dford5reg  35378  txpss3v  35474  brtxp  35476  brpprod  35481  brsset  35485  dfon3  35488  brtxpsd  35490  brtxpsd2  35491  dffun10  35510  elfuns  35511  funpartlem  35538  fullfunfv  35543  dfrdg4  35547  dfint3  35548  brub  35550  hfext  35779  neibastop2lem  35844  bj-equsexval  36136  bj-elid3  36646  finxp0  36870  finxp1o  36871  brvdif  37733  xrnss3v  37844  ntrneiel2  43516  ntrneik4w  43530  ismnushort  43738  funressnvmo  46427  dfdfat2  46508