Theorem mpbir2an 950

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 948	. 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  1201  euequ1  2174  eqssi  3242  elini  3390  dtruarb  4283  opnzi  4329  so0  4425  we0  4460  ord0  4490  ordon  4586  onsucelsucexmidlem1  4628  regexmidlemm  4632  ordpwsucexmid  4670  reg3exmidlemwe  4679  ordom  4707  funi  5360  funcnvsn  5377  funinsn  5381  fnresi  5452  fn0  5454  f0  5530  fconst  5535  f10  5621  f1o0  5625  f1oi  5626  f1osn  5628  funopsn  5833  isoid  5956  iso0  5963  acexmidlem2  6020  fo1st  6325  fo2nd  6326  iordsmo  6468  tfrlem7  6488  tfrexlem  6505  mapsnf1o2  6870  1domsn  7006  inresflem  7264  0ct  7311  infnninf  7328  infnninfOLD  7329  exmidonfinlem  7409  exmidaclem  7428  pw1on  7449  sucpw1nel3  7456  1pi  7540  prarloclemcalc  7727  ltsopr  7821  ltsosr  7989  cnm  8057  axicn  8088  axaddf  8093  axmulf  8094  nnindnn  8118  mpomulf  8174  ltso  8262  negiso  9140  nnind  9164  0z  9495  dfuzi  9595  cnref1o  9890  elrpii  9896  xrltso  10036  0e0icopnf  10219  0e0iccpnf  10220  fz0to4untppr  10364  fldiv4p1lem1div2  10571  expcl2lemap  10819  expclzaplem  10831  expge0  10843  expge1  10844  xrnegiso  11845  fclim  11877  eff2  12264  reeff1  12284  ef01bndlem  12340  sin01bnd  12341  cos01bnd  12342  sin01gt0  12346  egt2lt3  12364  halfleoddlt  12478  2prm  12722  3prm  12723  1arith  12963  setsslnid  13157  xpsff1o  13455  isabli  13910  rngmgpf  13974  mgpf  14048  zringnzr  14640  fntopon  14777  istpsi  14792  ismeti  15099  cnfldms  15289  tgqioo  15308  addcncntoplem  15314  divcnap  15318  abscncf  15338  recncf  15339  imcncf  15340  cjcncf  15341  maxcncf  15368  mincncf  15369  dveflem  15479  reeff1o  15526  reefiso  15530  ioocosf1o  15607  lgslem2  15759  lgsfcl2  15764  lgsne0  15796  2lgslem1b  15847  umgrbien  15990  konigsberglem1  16368  konigsberglem4  16371  ex-fl  16378  bj-indint  16586  bj-omord  16615  012of  16652  2o01f  16653  0nninf  16669  peano4nninf  16671  taupi  16745