Theorem mpbir2an 951

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 949	. 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  1202  euequ1  2176  eqssi  3253  elini  3402  dtruarb  4303  opnzi  4350  so0  4446  we0  4481  ord0  4511  ordon  4607  onsucelsucexmidlem1  4649  regexmidlemm  4653  ordpwsucexmid  4691  reg3exmidlemwe  4700  ordom  4728  funi  5383  funcnvsn  5400  funinsn  5404  fnresi  5475  fn0  5477  f0  5557  fconst  5562  f10  5648  f1o0  5652  f1oi  5653  f1osn  5655  funopsn  5859  isoid  5982  iso0  5989  acexmidlem2  6046  fo1st  6350  fo2nd  6351  iordsmo  6527  tfrlem7  6547  tfrexlem  6564  mapsnf1o2  6930  1domsn  7067  inresflem  7350  0ct  7397  infnninf  7414  infnninfOLD  7415  exmidonfinlem  7495  exmidaclem  7514  pw1on  7535  sucpw1nel3  7542  1pi  7626  prarloclemcalc  7813  ltsopr  7907  ltsosr  8075  cnm  8143  axicn  8174  axaddf  8179  axmulf  8180  nnindnn  8204  mpomulf  8260  ltso  8347  negiso  9225  nnind  9249  0z  9584  dfuzi  9684  cnref1o  9979  elrpii  9985  xrltso  10125  0e0icopnf  10308  0e0iccpnf  10309  fz0to4untppr  10454  fldiv4p1lem1div2  10661  expcl2lemap  10909  expclzaplem  10921  expge0  10933  expge1  10934  xrnegiso  11940  fclim  11972  eff2  12359  reeff1  12379  ef01bndlem  12435  sin01bnd  12436  cos01bnd  12437  sin01gt0  12441  egt2lt3  12459  halfleoddlt  12573  2prm  12817  3prm  12818  1arith  13058  setsslnid  13253  xpsff1o  13551  isabli  14006  rngmgpf  14070  mgpf  14144  zringnzr  14737  fntopon  14876  istpsi  14891  ismeti  15198  cnfldms  15388  tgqioo  15407  addcncntoplem  15413  divcnap  15417  abscncf  15437  recncf  15438  imcncf  15439  cjcncf  15440  maxcncf  15467  mincncf  15468  dveflem  15578  reeff1o  15625  reefiso  15629  ioocosf1o  15706  lgslem2  15861  lgsfcl2  15866  lgsne0  15898  2lgslem1b  15949  umgrbien  16092  konigsberglem1  16470  konigsberglem4  16473  ex-fl  16480  bj-indint  16688  bj-omord  16717  012of  16754  2o01f  16755  0nninf  16769  peano4nninf  16771  taupi  16845