Theorem mpbir2an 944

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 942	. 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  1177  euequ1  2140  eqssi  3200  elini  3348  dtruarb  4225  opnzi  4269  so0  4362  we0  4397  ord0  4427  ordon  4523  onsucelsucexmidlem1  4565  regexmidlemm  4569  ordpwsucexmid  4607  reg3exmidlemwe  4616  ordom  4644  funi  5291  funcnvsn  5304  funinsn  5308  fnresi  5378  fn0  5380  f0  5451  fconst  5456  f10  5541  f1o0  5544  f1oi  5545  f1osn  5547  isoid  5860  iso0  5867  acexmidlem2  5922  fo1st  6224  fo2nd  6225  iordsmo  6364  tfrlem7  6384  tfrexlem  6401  mapsnf1o2  6764  1domsn  6887  inresflem  7135  0ct  7182  infnninf  7199  infnninfOLD  7200  exmidonfinlem  7274  exmidaclem  7293  pw1on  7311  sucpw1nel3  7318  1pi  7401  prarloclemcalc  7588  ltsopr  7682  ltsosr  7850  cnm  7918  axicn  7949  axaddf  7954  axmulf  7955  nnindnn  7979  mpomulf  8035  ltso  8123  negiso  9001  nnind  9025  0z  9356  dfuzi  9455  cnref1o  9744  elrpii  9750  xrltso  9890  0e0icopnf  10073  0e0iccpnf  10074  fz0to4untppr  10218  fldiv4p1lem1div2  10414  expcl2lemap  10662  expclzaplem  10674  expge0  10686  expge1  10687  xrnegiso  11446  fclim  11478  eff2  11864  reeff1  11884  ef01bndlem  11940  sin01bnd  11941  cos01bnd  11942  sin01gt0  11946  egt2lt3  11964  halfleoddlt  12078  2prm  12322  3prm  12323  1arith  12563  setsslnid  12757  xpsff1o  13053  isabli  13508  rngmgpf  13571  mgpf  13645  zringnzr  14236  fntopon  14346  istpsi  14361  ismeti  14668  cnfldms  14858  tgqioo  14877  addcncntoplem  14883  divcnap  14887  abscncf  14907  recncf  14908  imcncf  14909  cjcncf  14910  maxcncf  14937  mincncf  14938  dveflem  15048  reeff1o  15095  reefiso  15099  ioocosf1o  15176  lgslem2  15328  lgsfcl2  15333  lgsne0  15365  2lgslem1b  15416  ex-fl  15457  bj-indint  15663  bj-omord  15692  012of  15726  2o01f  15727  0nninf  15737  peano4nninf  15739  taupi  15808