Theorem mpbir2an 947

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 945	. 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  1180  euequ1  2153  eqssi  3220  elini  3368  dtruarb  4254  opnzi  4300  so0  4394  we0  4429  ord0  4459  ordon  4555  onsucelsucexmidlem1  4597  regexmidlemm  4601  ordpwsucexmid  4639  reg3exmidlemwe  4648  ordom  4676  funi  5326  funcnvsn  5342  funinsn  5346  fnresi  5417  fn0  5419  f0  5492  fconst  5497  f10  5582  f1o0  5586  f1oi  5587  f1osn  5589  funopsn  5790  isoid  5907  iso0  5914  acexmidlem2  5971  fo1st  6273  fo2nd  6274  iordsmo  6413  tfrlem7  6433  tfrexlem  6450  mapsnf1o2  6813  1domsn  6946  inresflem  7195  0ct  7242  infnninf  7259  infnninfOLD  7260  exmidonfinlem  7339  exmidaclem  7358  pw1on  7379  sucpw1nel3  7386  1pi  7470  prarloclemcalc  7657  ltsopr  7751  ltsosr  7919  cnm  7987  axicn  8018  axaddf  8023  axmulf  8024  nnindnn  8048  mpomulf  8104  ltso  8192  negiso  9070  nnind  9094  0z  9425  dfuzi  9525  cnref1o  9814  elrpii  9820  xrltso  9960  0e0icopnf  10143  0e0iccpnf  10144  fz0to4untppr  10288  fldiv4p1lem1div2  10492  expcl2lemap  10740  expclzaplem  10752  expge0  10764  expge1  10765  xrnegiso  11739  fclim  11771  eff2  12157  reeff1  12177  ef01bndlem  12233  sin01bnd  12234  cos01bnd  12235  sin01gt0  12239  egt2lt3  12257  halfleoddlt  12371  2prm  12615  3prm  12616  1arith  12856  setsslnid  13050  xpsff1o  13348  isabli  13803  rngmgpf  13866  mgpf  13940  zringnzr  14531  fntopon  14663  istpsi  14678  ismeti  14985  cnfldms  15175  tgqioo  15194  addcncntoplem  15200  divcnap  15204  abscncf  15224  recncf  15225  imcncf  15226  cjcncf  15227  maxcncf  15254  mincncf  15255  dveflem  15365  reeff1o  15412  reefiso  15416  ioocosf1o  15493  lgslem2  15645  lgsfcl2  15650  lgsne0  15682  2lgslem1b  15733  umgrbien  15875  ex-fl  15999  bj-indint  16204  bj-omord  16233  012of  16268  2o01f  16269  0nninf  16281  peano4nninf  16283  taupi  16352