Theorem mpbiran 715

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

Syntax hints:   ↔ wb 207   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  mpbiran2  716  mpbir2an  717  pm5.63  1027  equsexALT  2427  velcomp  3905  0pss  4382  pssv  4384  disj4  4394  pwpwab  5039  zfpair  5357  opabn0  5502  relop  5799  ssrnres  6136  funopab  6527  funcnv2  6560  fnres  6619  dffv2  6929  funcnvmpt  6944  idref  7095  rnoprab  7468  suppssr  8142  frrlem9  8241  brwitnlem  8439  omeu  8517  naddcllem  8609  elixp  8849  dfsup2  9354  card2inf  9467  harndom  9474  dford2  9539  cantnfp1lem3  9599  cantnfp1  9600  cantnflem1  9608  ttrclresv  9636  tz9.12lem3  9711  djulf1o  9834  djurf1o  9835  dfac4  10042  dfac12a  10069  cflem  10165  cflemOLD  10166  cfsmolem  10190  dffin7-2  10318  dfacfin7  10319  brdom3  10448  iunfo  10459  gch3  10597  lbfzo0  13652  fzo1lb  13666  1elfzo1  13667  gcdcllem3  16468  1nprm  16646  cygctb  19865  expmhm  21418  expghm  21457  opsrtoslem2  22039  mat1dimelbas  22461  basdif0  22943  txdis1cn  23625  trfil2  23877  txflf  23996  clsnsg  24100  tgpconncomp  24103  perfdvf  25895  wilthlem3  27058  noeta2  27778  sltssnb  27786  etaslts2  27811  made0  27880  bdayons  28293  noseqind  28309  zsoring  28426  mpteleeOLD  28989  iscplgr  29509  rgrprcx  29686  blocnilem  30900  h1de2i  31649  nmop0  32082  nmfn0  32083  lnopconi  32130  lnfnconi  32151  stcltr2i  32371  1stpreima  32806  2ndpreima  32807  suppss3  32822  onvf1od  35336  fmla0  35611  fmlasuc0  35613  elmrsubrn  35749  dftr6  35980  br6  35986  dford5reg  36009  txpss3v  36105  brtxp  36107  brpprod  36112  brsset  36116  dfon3  36119  brtxpsd  36121  brtxpsd2  36122  dffun10  36141  elfuns  36142  funpartlem  36171  fullfunfv  36176  dfrdg4  36180  dfint3  36181  brub  36183  hfext  36412  neibastop2lem  36589  bj-equsexval  37001  bj-elid3  37528  finxp0  37754  finxp1o  37755  brvdif  38634  xrnss3v  38749  ntrneiel2  44531  ntrneik4w  44545  ismnushort  44746  permaxpow  45454  funressnvmo  47509  dfdfat2  47592