Theorem mpbir2an 948

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 946	. 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  1199  euequ1  2173  eqssi  3241  elini  3389  dtruarb  4279  opnzi  4325  so0  4421  we0  4456  ord0  4486  ordon  4582  onsucelsucexmidlem1  4624  regexmidlemm  4628  ordpwsucexmid  4666  reg3exmidlemwe  4675  ordom  4703  funi  5356  funcnvsn  5372  funinsn  5376  fnresi  5447  fn0  5449  f0  5524  fconst  5529  f10  5614  f1o0  5618  f1oi  5619  f1osn  5621  funopsn  5825  isoid  5946  iso0  5953  acexmidlem2  6010  fo1st  6315  fo2nd  6316  iordsmo  6458  tfrlem7  6478  tfrexlem  6495  mapsnf1o2  6860  1domsn  6996  inresflem  7253  0ct  7300  infnninf  7317  infnninfOLD  7318  exmidonfinlem  7397  exmidaclem  7416  pw1on  7437  sucpw1nel3  7444  1pi  7528  prarloclemcalc  7715  ltsopr  7809  ltsosr  7977  cnm  8045  axicn  8076  axaddf  8081  axmulf  8082  nnindnn  8106  mpomulf  8162  ltso  8250  negiso  9128  nnind  9152  0z  9483  dfuzi  9583  cnref1o  9878  elrpii  9884  xrltso  10024  0e0icopnf  10207  0e0iccpnf  10208  fz0to4untppr  10352  fldiv4p1lem1div2  10558  expcl2lemap  10806  expclzaplem  10818  expge0  10830  expge1  10831  xrnegiso  11816  fclim  11848  eff2  12234  reeff1  12254  ef01bndlem  12310  sin01bnd  12311  cos01bnd  12312  sin01gt0  12316  egt2lt3  12334  halfleoddlt  12448  2prm  12692  3prm  12693  1arith  12933  setsslnid  13127  xpsff1o  13425  isabli  13880  rngmgpf  13943  mgpf  14017  zringnzr  14609  fntopon  14741  istpsi  14756  ismeti  15063  cnfldms  15253  tgqioo  15272  addcncntoplem  15278  divcnap  15282  abscncf  15302  recncf  15303  imcncf  15304  cjcncf  15305  maxcncf  15332  mincncf  15333  dveflem  15443  reeff1o  15490  reefiso  15494  ioocosf1o  15571  lgslem2  15723  lgsfcl2  15728  lgsne0  15760  2lgslem1b  15811  umgrbien  15954  ex-fl  16271  bj-indint  16476  bj-omord  16505  012of  16542  2o01f  16543  0nninf  16556  peano4nninf  16558  taupi  16627