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  2450  velcomp  3917  0pss  4363  pssv  4365  disj4  4415  pwpwab  5067  zfpair  5390  opabn0  5536  relop  5834  ssrnres  6175  funopab  6572  funcnv2  6605  fnres  6663  dffv2  6977  funcnvmpt  6992  idref  7145  rnoprab  7521  suppssr  8196  frrlem9  8296  brwitnlem  8497  omeu  8575  naddcllem  8667  elixp  8914  dfsup2  9417  card2inf  9530  harndom  9537  dford2  9602  cantnfp1lem3  9662  cantnfp1  9663  cantnflem1  9671  ttrclresv  9699  tz9.12lem3  9774  djulf1o  9920  djurf1o  9921  dfac4  10128  dfac12a  10154  cflem  10250  cfsmolem  10275  dffin7-2  10403  dfacfin7  10404  brdom3  10534  iunfo  10550  gch3  10688  lbfzo0  13757  fzo1lb  13771  1elfzo1  13772  gcdcllem3  16595  1nprm  16773  cygctb  20023  expmhm  21653  expghm  21692  opsrtoslem2  22276  mat1dimelbas  22697  basdif0  23182  txdis1cn  23865  trfil2  24117  txflf  24236  clsnsg  24340  tgpconncomp  24343  perfdvf  26135  wilthlem3  27307  noeta2  28027  sltssnb  28035  etaslts2  28060  made0  28129  bdayons  28542  noseqind  28558  zsoring  28675  mpteleeOLD  29353  iscplgr  29876  rgrprcx  30053  blocnilem  31286  h1de2i  32035  nmop0  32468  nmfn0  32469  lnopconi  32516  lnfnconi  32537  stcltr2i  32757  1stpreima  33181  2ndpreima  33182  suppss3  33196  onvf1od  35706  vonf1oonfo  35714  fmla0  35963  fmlasuc0  35965  elmrsubrn  36101  dftr6  36332  br6  36338  dford5reg  36361  txpss3v  36457  brtxp  36459  brpprod  36464  brsset  36468  dfon3  36471  brtxpsd  36473  brtxpsd2  36474  dffun10  36493  elfuns  36494  funpartlem  36523  fullfunfv  36528  dfrdg4  36532  dfint3  36533  brub  36535  dffr7  36537  hfext  36765  neibastop2lem  36981  bj-equsexval  37392  bj-elid3  37921  finxp0  38147  finxp1o  38148  brvdif  39016  xrnss3v  39131  ntrneiel2  44928  ntrneik4w  44942  ismnushort  45127  permaxpow  45834  funressnvmo  47935  dfdfat2  48018