Theorem mpbir2an 950

Description: Detach a conjunction of truths in a biconditional. (Contributed by NM, 10-May-2005.) (Revised by NM, 9-Jan-2015.)

Hypotheses

Ref	Expression
mpbir2an.1	⊢ 𝜓
mpbir2an.2	⊢ 𝜒
mpbiran2an.1	⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))

Assertion

Ref	Expression
mpbir2an	⊢ 𝜑

Proof of Theorem mpbir2an

Step	Hyp	Ref	Expression
1		mpbir2an.2	. 2 ⊢ 𝜒
2		mpbir2an.1	. . 3 ⊢ 𝜓
3		mpbiran2an.1	. . 3 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))
4	2, 3	mpbiran 948	. 2 ⊢ (𝜑 ↔ 𝜒)
5	1, 4	mpbir 146	1 ⊢ 𝜑

Syntax hints:   ∧ wa 104   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  3pm3.2i  1201  euequ1  2175  eqssi  3243  elini  3391  dtruarb  4281  opnzi  4327  so0  4423  we0  4458  ord0  4488  ordon  4584  onsucelsucexmidlem1  4626  regexmidlemm  4630  ordpwsucexmid  4668  reg3exmidlemwe  4677  ordom  4705  funi  5358  funcnvsn  5375  funinsn  5379  fnresi  5450  fn0  5452  f0  5527  fconst  5532  f10  5618  f1o0  5622  f1oi  5623  f1osn  5625  funopsn  5830  isoid  5951  iso0  5958  acexmidlem2  6015  fo1st  6320  fo2nd  6321  iordsmo  6463  tfrlem7  6483  tfrexlem  6500  mapsnf1o2  6865  1domsn  7001  inresflem  7259  0ct  7306  infnninf  7323  infnninfOLD  7324  exmidonfinlem  7404  exmidaclem  7423  pw1on  7444  sucpw1nel3  7451  1pi  7535  prarloclemcalc  7722  ltsopr  7816  ltsosr  7984  cnm  8052  axicn  8083  axaddf  8088  axmulf  8089  nnindnn  8113  mpomulf  8169  ltso  8257  negiso  9135  nnind  9159  0z  9490  dfuzi  9590  cnref1o  9885  elrpii  9891  xrltso  10031  0e0icopnf  10214  0e0iccpnf  10215  fz0to4untppr  10359  fldiv4p1lem1div2  10566  expcl2lemap  10814  expclzaplem  10826  expge0  10838  expge1  10839  xrnegiso  11824  fclim  11856  eff2  12243  reeff1  12263  ef01bndlem  12319  sin01bnd  12320  cos01bnd  12321  sin01gt0  12325  egt2lt3  12343  halfleoddlt  12457  2prm  12701  3prm  12702  1arith  12942  setsslnid  13136  xpsff1o  13434  isabli  13889  rngmgpf  13953  mgpf  14027  zringnzr  14619  fntopon  14751  istpsi  14766  ismeti  15073  cnfldms  15263  tgqioo  15282  addcncntoplem  15288  divcnap  15292  abscncf  15312  recncf  15313  imcncf  15314  cjcncf  15315  maxcncf  15342  mincncf  15343  dveflem  15453  reeff1o  15500  reefiso  15504  ioocosf1o  15581  lgslem2  15733  lgsfcl2  15738  lgsne0  15770  2lgslem1b  15821  umgrbien  15964  ex-fl  16338  bj-indint  16547  bj-omord  16576  012of  16613  2o01f  16614  0nninf  16627  peano4nninf  16629  taupi  16698