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  3258  elini  3407  dtruarb  4310  opnzi  4357  so0  4453  we0  4488  ord0  4518  ordon  4615  onsucelsucexmidlem1  4657  regexmidlemm  4661  ordpwsucexmid  4699  reg3exmidlemwe  4708  ordom  4736  funi  5391  funcnvsn  5408  funinsn  5412  fnresi  5483  fn0  5485  f0  5565  fconst  5570  f10  5656  f1o0  5660  f1oi  5661  f1osn  5663  funopsn  5867  isoid  5991  iso0  5998  rinvf1o  6010  acexmidlem2  6057  fo1st  6366  fo2nd  6367  iordsmo  6543  tfrlem7  6563  tfrexlem  6580  mapsnf1o2  6946  1domsn  7083  inresflem  7366  0ct  7413  infnninf  7430  infnninfOLD  7431  exmidonfinlem  7511  exmidaclem  7530  pw1on  7551  sucpw1nel3  7558  1pi  7648  prarloclemcalc  7835  ltsopr  7929  ltsosr  8097  cnm  8165  axicn  8196  axaddf  8201  axmulf  8202  nnindnn  8226  mpomulf  8282  ltso  8369  negiso  9251  nnind  9275  0z  9610  dfuzi  9711  cnref1o  10006  elrpii  10012  xrltso  10153  0e0icopnf  10336  0e0iccpnf  10337  fz0to4untppr  10485  fldiv4p1lem1div2  10694  expcl2lemap  10942  expclzaplem  10954  expge0  10966  expge1  10967  xrnegiso  11978  fclim  12010  eff2  12397  reeff1  12417  ef01bndlem  12473  sin01bnd  12474  cos01bnd  12475  sin01gt0  12479  egt2lt3  12497  halfleoddlt  12611  2prm  12855  3prm  12856  1arith  13096  ballotfilemonn  13171  ballotfilem2  13178  setsslnid  13354  xpsff1o  13619  isabli  14052  rngmgpf  14183  mgpf  14261  zringnzr  14881  fntopon  15020  istpsi  15035  ismeti  15342  cnfldms  15532  tgqioo  15551  addcncntoplem  15557  divcnap  15561  abscncf  15581  recncf  15582  imcncf  15583  cjcncf  15584  maxcncf  15611  mincncf  15612  dveflem  15722  reeff1o  15769  reefiso  15773  ioocosf1o  15850  lgslem2  16006  lgsfcl2  16011  lgsne0  16043  2lgslem1b  16094  umgrbien  16237  konigsberglem1  16615  konigsberglem4  16618  ex-fl  16625  bj-indint  16843  bj-omord  16872  012of  16909  2o01f  16910  0nninf  16924  peano4nninf  16926  taupi  17000