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  2448  velcomp  4054  0pss  4359  pssv  4361  disj4  4411  pwpwab  5062  zfpair  5382  opabn0  5527  relop  5827  ssrnres  6169  funopab  6575  funcnv2  6608  fnres  6666  dffv2  6980  funcnvmpt  6995  idref  7149  rnoprab  7525  suppssr  8213  frrlem9  8313  brwitnlem  8516  omeu  8594  naddcllem  8686  elixp  8933  dfsup2  9437  card2inf  9550  harndom  9557  dford2  9622  cantnfp1lem3  9682  cantnfp1  9683  cantnflem1  9691  ttrclresv  9719  tz9.12lem3  9797  djulf1o  9994  djurf1o  9995  dfac4  10202  dfac12a  10228  cflem  10324  cfsmolem  10349  dffin7-2  10477  dfacfin7  10478  brdom3  10608  iunfo  10624  gch3  10762  lbfzo0  13835  fzo1lb  13849  1elfzo1  13850  gcdcllem3  16672  1nprm  16855  cygctb  20107  expmhm  21743  expghm  21782  opsrtoslem2  22366  mat1dimelbas  22787  basdif0  23272  txdis1cn  23955  trfil2  24207  txflf  24326  clsnsg  24430  tgpconncomp  24433  perfdvf  26224  wilthlem3  27398  noeta2  28148  sltssnb  28156  etaslts2  28181  made0  28250  bdayons  28663  noseqind  28679  zsoring  28796  mpteleeOLD  29474  iscplgr  29997  rgrprcx  30174  blocnilem  31407  h1de2i  32156  nmop0  32589  nmfn0  32590  lnopconi  32637  lnfnconi  32658  stcltr2i  32878  1stpreima  33343  2ndpreima  33344  suppss3  33358  rncardr1prc  35807  acwer1prc  35809  onvf1od  35947  vonf1oonfo  35961  fmla0  36216  fmlasuc0  36218  elmrsubrn  36354  dftr6  36591  br6  36597  dford5reg  36619  txpss3v  36715  brtxp  36717  brpprod  36722  brsset  36726  dfon3  36729  brtxpsd  36731  brtxpsd2  36732  dffun10  36751  elfuns  36752  funpartlem  36781  fullfunfv  36786  dfrdg4  36790  dfint3  36791  brub  36793  dffr7  36795  hfext  37009  neibastop2lem  37223  mh-inf3f1  37404  bj-equsexval  37634  coi1in  38036  bj-elid3  38164  finxp0  38390  finxp1o  38391  brvdif  39274  xrnss3v  39389  ntrneiel2  45162  ntrneik4w  45176  ismnushort  45361  permaxpow  46075  funressnvmo  48191  dfdfat2  48274