Theorem mpbir2an 955

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

This proof depends on syntax axioms:   ∧ wa 104   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  3pm3.2i  1206  euequ1  2182  eqssi  3264  elini  3413  dtruarb  4328  opnzi  4375  so0  4471  we0  4506  ord0  4536  ordon  4633  onsucelsucexmidlem1  4675  regexmidlemm  4679  ordpwsucexmid  4717  reg3exmidlemwe  4726  ordom  4754  funi  5409  funcnvsn  5426  funinsn  5430  fnresi  5501  fn0  5503  f0  5583  fconst  5588  f10  5674  f1o0  5678  f1oi  5679  f1osn  5681  funopsn  5891  isoid  6016  iso0  6023  rinvf1o  6035  acexmidlem2  6082  fo1st  6391  fo2nd  6392  iordsmo  6568  tfrlem7  6588  tfrexlem  6605  mapsnf1o2  6978  1domsn  7115  inresflem  7400  0ct  7447  infnninf  7464  infnninfOLD  7465  exmidonfinlem  7545  exmidaclem  7564  pw1on  7585  sucpw1nel3  7592  1pi  7682  prarloclemcalc  7869  ltsopr  7963  ltsosr  8131  cnm  8199  axicn  8230  axaddf  8235  axmulf  8236  nnindnn  8260  mpomulf  8316  ltso  8403  negiso  9286  nnind  9321  0z  9657  dfuzi  9758  cnref1o  10053  elrpii  10059  xrltso  10200  0e0icopnf  10383  0e0iccpnf  10384  fz0to4untppr  10533  fldiv4p1lem1div2  10742  expcl2lemap  10990  expclzaplem  11002  expge0  11014  expge1  11015  xrnegiso  12030  fclim  12062  eff2  12449  reeff1  12469  ef01bndlem  12525  sin01bnd  12526  cos01bnd  12527  sin01gt0  12531  egt2lt3  12549  halfleoddlt  12663  2prm  12907  3prm  12908  1arith  13148  ballotfilemonn  13223  ballotfilem2  13230  setsslnid  13406  xpsff1o  13672  isabli  14105  rngmgpf  14238  mgpf  14317  zringnzr  14939  fntopon  15127  istpsi  15142  ismeti  15449  cnfldms  15639  tgqioo  15658  addcncntoplem  15664  divcnap  15668  abscncf  15688  recncf  15689  imcncf  15690  cjcncf  15691  maxcncf  15718  mincncf  15719  dveflem  15829  reeff1o  15876  reefiso  15880  ioocosf1o  15958  lgslem2  16132  lgsfcl2  16137  lgsne0  16169  2lgslem1b  16220  umgrbien  16363  konigsberglem1  16741  konigsberglem4  16744  ex-fl  16751  bj-indint  16969  bj-omord  16998  012of  17035  2o01f  17036  0nninf  17059  peano4nninf  17061  taupi  17135