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 ⊢ 𝜑

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  1206  euequ1  2182  eqssi  3264  elini  3413  dtruarb  4326  opnzi  4373  so0  4469  we0  4504  ord0  4534  ordon  4631  onsucelsucexmidlem1  4673  regexmidlemm  4677  ordpwsucexmid  4715  reg3exmidlemwe  4724  ordom  4752  funi  5407  funcnvsn  5424  funinsn  5428  fnresi  5499  fn0  5501  f0  5581  fconst  5586  f10  5672  f1o0  5676  f1oi  5677  f1osn  5679  funopsn  5885  isoid  6010  iso0  6017  rinvf1o  6029  acexmidlem2  6076  fo1st  6385  fo2nd  6386  iordsmo  6562  tfrlem7  6582  tfrexlem  6599  mapsnf1o2  6972  1domsn  7109  inresflem  7394  0ct  7441  infnninf  7458  infnninfOLD  7459  exmidonfinlem  7539  exmidaclem  7558  pw1on  7579  sucpw1nel3  7586  1pi  7676  prarloclemcalc  7863  ltsopr  7957  ltsosr  8125  cnm  8193  axicn  8224  axaddf  8229  axmulf  8230  nnindnn  8254  mpomulf  8310  ltso  8397  negiso  9279  nnind  9303  0z  9638  dfuzi  9739  cnref1o  10034  elrpii  10040  xrltso  10181  0e0icopnf  10364  0e0iccpnf  10365  fz0to4untppr  10514  fldiv4p1lem1div2  10723  expcl2lemap  10971  expclzaplem  10983  expge0  10995  expge1  10996  xrnegiso  12011  fclim  12043  eff2  12430  reeff1  12450  ef01bndlem  12506  sin01bnd  12507  cos01bnd  12508  sin01gt0  12512  egt2lt3  12530  halfleoddlt  12644  2prm  12888  3prm  12889  1arith  13129  ballotfilemonn  13204  ballotfilem2  13211  setsslnid  13387  xpsff1o  13653  isabli  14086  rngmgpf  14219  mgpf  14298  zringnzr  14920  fntopon  15108  istpsi  15123  ismeti  15430  cnfldms  15620  tgqioo  15639  addcncntoplem  15645  divcnap  15649  abscncf  15669  recncf  15670  imcncf  15671  cjcncf  15672  maxcncf  15699  mincncf  15700  dveflem  15810  reeff1o  15857  reefiso  15861  ioocosf1o  15938  lgslem2  16103  lgsfcl2  16108  lgsne0  16140  2lgslem1b  16191  umgrbien  16334  konigsberglem1  16712  konigsberglem4  16715  ex-fl  16722  bj-indint  16940  bj-omord  16969  012of  17006  2o01f  17007  0nninf  17021  peano4nninf  17023  taupi  17097