Theorem mpbir2an 945

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 943	. 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  1178  euequ1  2150  eqssi  3210  elini  3358  dtruarb  4239  opnzi  4283  so0  4377  we0  4412  ord0  4442  ordon  4538  onsucelsucexmidlem1  4580  regexmidlemm  4584  ordpwsucexmid  4622  reg3exmidlemwe  4631  ordom  4659  funi  5308  funcnvsn  5324  funinsn  5328  fnresi  5399  fn0  5401  f0  5473  fconst  5478  f10  5563  f1o0  5566  f1oi  5567  f1osn  5569  funopsn  5769  isoid  5886  iso0  5893  acexmidlem2  5948  fo1st  6250  fo2nd  6251  iordsmo  6390  tfrlem7  6410  tfrexlem  6427  mapsnf1o2  6790  1domsn  6921  inresflem  7169  0ct  7216  infnninf  7233  infnninfOLD  7234  exmidonfinlem  7308  exmidaclem  7327  pw1on  7345  sucpw1nel3  7352  1pi  7435  prarloclemcalc  7622  ltsopr  7716  ltsosr  7884  cnm  7952  axicn  7983  axaddf  7988  axmulf  7989  nnindnn  8013  mpomulf  8069  ltso  8157  negiso  9035  nnind  9059  0z  9390  dfuzi  9490  cnref1o  9779  elrpii  9785  xrltso  9925  0e0icopnf  10108  0e0iccpnf  10109  fz0to4untppr  10253  fldiv4p1lem1div2  10455  expcl2lemap  10703  expclzaplem  10715  expge0  10727  expge1  10728  xrnegiso  11617  fclim  11649  eff2  12035  reeff1  12055  ef01bndlem  12111  sin01bnd  12112  cos01bnd  12113  sin01gt0  12117  egt2lt3  12135  halfleoddlt  12249  2prm  12493  3prm  12494  1arith  12734  setsslnid  12928  xpsff1o  13225  isabli  13680  rngmgpf  13743  mgpf  13817  zringnzr  14408  fntopon  14540  istpsi  14555  ismeti  14862  cnfldms  15052  tgqioo  15071  addcncntoplem  15077  divcnap  15081  abscncf  15101  recncf  15102  imcncf  15103  cjcncf  15104  maxcncf  15131  mincncf  15132  dveflem  15242  reeff1o  15289  reefiso  15293  ioocosf1o  15370  lgslem2  15522  lgsfcl2  15527  lgsne0  15559  2lgslem1b  15610  ex-fl  15735  bj-indint  15941  bj-omord  15970  012of  16004  2o01f  16005  0nninf  16015  peano4nninf  16017  taupi  16086