Theorem mpbir2an 932

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 930	. 2 ⊢ (𝜑 ↔ 𝜒)
5	1, 4	mpbir 145	1 ⊢ 𝜑

Syntax hints:   ∧ wa 103   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3pm3.2i  1165  euequ1  2109  eqssi  3157  elini  3305  dtruarb  4169  opnzi  4212  so0  4303  we0  4338  ord0  4368  ordon  4462  onsucelsucexmidlem1  4504  regexmidlemm  4508  ordpwsucexmid  4546  reg3exmidlemwe  4555  ordom  4583  funi  5219  funcnvsn  5232  funinsn  5236  fnresi  5304  fn0  5306  f0  5377  fconst  5382  f10  5465  f1o0  5468  f1oi  5469  f1osn  5471  isoid  5777  iso0  5784  acexmidlem2  5838  fo1st  6122  fo2nd  6123  iordsmo  6261  tfrlem7  6281  tfrexlem  6298  mapsnf1o2  6658  1domsn  6781  inresflem  7021  0ct  7068  infnninf  7084  infnninfOLD  7085  exmidonfinlem  7145  exmidaclem  7160  pw1on  7178  sucpw1nel3  7185  1pi  7252  prarloclemcalc  7439  ltsopr  7533  ltsosr  7701  cnm  7769  axicn  7800  axaddf  7805  axmulf  7806  nnindnn  7830  ltso  7972  negiso  8846  nnind  8869  0z  9198  dfuzi  9297  cnref1o  9584  elrpii  9588  xrltso  9728  0e0icopnf  9911  0e0iccpnf  9912  fz0to4untppr  10055  fldiv4p1lem1div2  10236  expcl2lemap  10463  expclzaplem  10475  expge0  10487  expge1  10488  xrnegiso  11199  fclim  11231  eff2  11617  reeff1  11637  ef01bndlem  11693  sin01bnd  11694  cos01bnd  11695  sin01gt0  11698  egt2lt3  11716  halfleoddlt  11827  2prm  12055  3prm  12056  1arith  12293  setsslnid  12441  fntopon  12622  istpsi  12637  ismeti  12946  tgqioo  13147  addcncntoplem  13151  divcnap  13155  abscncf  13172  recncf  13173  imcncf  13174  cjcncf  13175  dveflem  13287  reeff1o  13294  reefiso  13298  ioocosf1o  13375  lgslem2  13502  lgsfcl2  13507  lgsne0  13539  ex-fl  13566  bj-indint  13773  bj-omord  13802  012of  13835  2o01f  13836  0nninf  13844  peano4nninf  13846  taupi  13909