Theorem mpbir2an 891

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

Syntax hints:   ∧ wa 103   ↔ wb 104

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 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  1124  euequ1  2050  eqssi  3055  elini  3199  dtruarb  4047  opnzi  4086  so0  4177  we0  4212  ord0  4242  ordon  4331  onsucelsucexmidlem1  4372  regexmidlemm  4376  ordpwsucexmid  4414  reg3exmidlemwe  4422  ordom  4449  funi  5080  funcnvsn  5093  funinsn  5097  fnresi  5165  fn0  5167  f0  5236  fconst  5241  f10  5322  f1o0  5325  f1oi  5326  f1osn  5328  isoid  5627  iso0  5634  acexmidlem2  5687  fo1st  5966  fo2nd  5967  iordsmo  6100  tfrlem7  6120  tfrexlem  6137  mapsnf1o2  6493  1domsn  6615  inresflem  6832  0ct  6869  infnninf  6893  1pi  6971  prarloclemcalc  7158  ltsopr  7252  ltsosr  7407  axicn  7497  nnindnn  7525  ltso  7660  negiso  8513  nnind  8536  0z  8859  dfuzi  8955  cnref1o  9232  elrpii  9236  xrltso  9365  0e0icopnf  9545  0e0iccpnf  9546  fldiv4p1lem1div2  9861  expcl2lemap  10082  expclzaplem  10094  expge0  10106  expge1  10107  xrnegiso  10805  fclim  10837  eff2  11119  reeff1  11140  ef01bndlem  11196  sin01bnd  11197  cos01bnd  11198  sin01gt0  11201  egt2lt3  11216  halfleoddlt  11321  2prm  11536  3prm  11537  setsslnid  11694  fntopon  11874  istpsi  11889  ismeti  12132  tgqioo  12321  abscncf  12338  recncf  12339  imcncf  12340  cjcncf  12341  ex-fl  12360  bj-indint  12534  bj-omord  12563  0nninf  12598  peano4nninf  12601