Theorem mpbir2an 926

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 924	. 2 ⊢ (𝜑 ↔ 𝜒)
5	1, 4	mpbir 145	1 ⊢ 𝜑

Syntax hints:   ∧ wa 103   ↔ wb 104

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3pm3.2i  1159  euequ1  2092  eqssi  3108  elini  3255  dtruarb  4110  opnzi  4152  so0  4243  we0  4278  ord0  4308  ordon  4397  onsucelsucexmidlem1  4438  regexmidlemm  4442  ordpwsucexmid  4480  reg3exmidlemwe  4488  ordom  4515  funi  5150  funcnvsn  5163  funinsn  5167  fnresi  5235  fn0  5237  f0  5308  fconst  5313  f10  5394  f1o0  5397  f1oi  5398  f1osn  5400  isoid  5704  iso0  5711  acexmidlem2  5764  fo1st  6048  fo2nd  6049  iordsmo  6187  tfrlem7  6207  tfrexlem  6224  mapsnf1o2  6583  1domsn  6706  inresflem  6938  0ct  6985  infnninf  7015  exmidonfinlem  7042  exmidaclem  7057  1pi  7116  prarloclemcalc  7303  ltsopr  7397  ltsosr  7565  cnm  7633  axicn  7664  axaddf  7669  axmulf  7670  nnindnn  7694  ltso  7835  negiso  8706  nnind  8729  0z  9058  dfuzi  9154  cnref1o  9433  elrpii  9437  xrltso  9575  0e0icopnf  9755  0e0iccpnf  9756  fldiv4p1lem1div2  10071  expcl2lemap  10298  expclzaplem  10310  expge0  10322  expge1  10323  xrnegiso  11024  fclim  11056  eff2  11375  reeff1  11396  ef01bndlem  11452  sin01bnd  11453  cos01bnd  11454  sin01gt0  11457  egt2lt3  11475  halfleoddlt  11580  2prm  11797  3prm  11798  setsslnid  11999  fntopon  12180  istpsi  12195  ismeti  12504  tgqioo  12705  addcncntoplem  12709  divcnap  12713  abscncf  12730  recncf  12731  imcncf  12732  cjcncf  12733  dveflem  12844  ex-fl  12926  bj-indint  13118  bj-omord  13147  0nninf  13186  peano4nninf  13189  isomninnlem  13214  taupi  13228