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  3256  elini  3405  dtruarb  4306  opnzi  4353  so0  4449  we0  4484  ord0  4514  ordon  4610  onsucelsucexmidlem1  4652  regexmidlemm  4656  ordpwsucexmid  4694  reg3exmidlemwe  4703  ordom  4731  funi  5386  funcnvsn  5403  funinsn  5407  fnresi  5478  fn0  5480  f0  5560  fconst  5565  f10  5651  f1o0  5655  f1oi  5656  f1osn  5658  funopsn  5862  isoid  5985  iso0  5992  acexmidlem2  6049  fo1st  6353  fo2nd  6354  iordsmo  6530  tfrlem7  6550  tfrexlem  6567  mapsnf1o2  6933  1domsn  7070  inresflem  7353  0ct  7400  infnninf  7417  infnninfOLD  7418  exmidonfinlem  7498  exmidaclem  7517  pw1on  7538  sucpw1nel3  7545  1pi  7635  prarloclemcalc  7822  ltsopr  7916  ltsosr  8084  cnm  8152  axicn  8183  axaddf  8188  axmulf  8189  nnindnn  8213  mpomulf  8269  ltso  8356  negiso  9234  nnind  9258  0z  9593  dfuzi  9694  cnref1o  9989  elrpii  9995  xrltso  10135  0e0icopnf  10318  0e0iccpnf  10319  fz0to4untppr  10465  fldiv4p1lem1div2  10672  expcl2lemap  10920  expclzaplem  10932  expge0  10944  expge1  10945  xrnegiso  11955  fclim  11987  eff2  12374  reeff1  12394  ef01bndlem  12450  sin01bnd  12451  cos01bnd  12452  sin01gt0  12456  egt2lt3  12474  halfleoddlt  12588  2prm  12832  3prm  12833  1arith  13073  ballotfilemonn  13148  ballotfilem2  13153  setsslnid  13285  xpsff1o  13583  isabli  14038  rngmgpf  14102  mgpf  14176  zringnzr  14799  fntopon  14938  istpsi  14953  ismeti  15260  cnfldms  15450  tgqioo  15469  addcncntoplem  15475  divcnap  15479  abscncf  15499  recncf  15500  imcncf  15501  cjcncf  15502  maxcncf  15529  mincncf  15530  dveflem  15640  reeff1o  15687  reefiso  15691  ioocosf1o  15768  lgslem2  15923  lgsfcl2  15928  lgsne0  15960  2lgslem1b  16011  umgrbien  16154  konigsberglem1  16532  konigsberglem4  16535  ex-fl  16542  bj-indint  16750  bj-omord  16779  012of  16816  2o01f  16817  0nninf  16831  peano4nninf  16833  taupi  16908