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  2178  eqssi  3258  elini  3407  dtruarb  4309  opnzi  4356  so0  4452  we0  4487  ord0  4517  ordon  4613  onsucelsucexmidlem1  4655  regexmidlemm  4659  ordpwsucexmid  4697  reg3exmidlemwe  4706  ordom  4734  funi  5389  funcnvsn  5406  funinsn  5410  fnresi  5481  fn0  5483  f0  5563  fconst  5568  f10  5654  f1o0  5658  f1oi  5659  f1osn  5661  funopsn  5865  isoid  5989  iso0  5996  rinvf1o  6008  acexmidlem2  6055  fo1st  6364  fo2nd  6365  iordsmo  6541  tfrlem7  6561  tfrexlem  6578  mapsnf1o2  6944  1domsn  7081  inresflem  7364  0ct  7411  infnninf  7428  infnninfOLD  7429  exmidonfinlem  7509  exmidaclem  7528  pw1on  7549  sucpw1nel3  7556  1pi  7646  prarloclemcalc  7833  ltsopr  7927  ltsosr  8095  cnm  8163  axicn  8194  axaddf  8199  axmulf  8200  nnindnn  8224  mpomulf  8280  ltso  8367  negiso  9249  nnind  9273  0z  9608  dfuzi  9709  cnref1o  10004  elrpii  10010  xrltso  10151  0e0icopnf  10334  0e0iccpnf  10335  fz0to4untppr  10483  fldiv4p1lem1div2  10692  expcl2lemap  10940  expclzaplem  10952  expge0  10964  expge1  10965  xrnegiso  11975  fclim  12007  eff2  12394  reeff1  12414  ef01bndlem  12470  sin01bnd  12471  cos01bnd  12472  sin01gt0  12476  egt2lt3  12494  halfleoddlt  12608  2prm  12852  3prm  12853  1arith  13093  ballotfilemonn  13168  ballotfilem2  13175  setsslnid  13351  xpsff1o  13616  isabli  14056  rngmgpf  14179  mgpf  14257  zringnzr  14879  fntopon  15018  istpsi  15033  ismeti  15340  cnfldms  15530  tgqioo  15549  addcncntoplem  15555  divcnap  15559  abscncf  15579  recncf  15580  imcncf  15581  cjcncf  15582  maxcncf  15609  mincncf  15610  dveflem  15720  reeff1o  15767  reefiso  15771  ioocosf1o  15848  lgslem2  16003  lgsfcl2  16008  lgsne0  16040  2lgslem1b  16091  umgrbien  16234  konigsberglem1  16612  konigsberglem4  16615  ex-fl  16622  bj-indint  16840  bj-omord  16869  012of  16906  2o01f  16907  0nninf  16921  peano4nninf  16923  taupi  16998