Theorem mpbir2an 944

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 942	. 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  1177  euequ1  2140  eqssi  3199  elini  3347  dtruarb  4224  opnzi  4268  so0  4361  we0  4396  ord0  4426  ordon  4522  onsucelsucexmidlem1  4564  regexmidlemm  4568  ordpwsucexmid  4606  reg3exmidlemwe  4615  ordom  4643  funi  5290  funcnvsn  5303  funinsn  5307  fnresi  5375  fn0  5377  f0  5448  fconst  5453  f10  5538  f1o0  5541  f1oi  5542  f1osn  5544  isoid  5857  iso0  5864  acexmidlem2  5919  fo1st  6215  fo2nd  6216  iordsmo  6355  tfrlem7  6375  tfrexlem  6392  mapsnf1o2  6755  1domsn  6878  inresflem  7126  0ct  7173  infnninf  7190  infnninfOLD  7191  exmidonfinlem  7260  exmidaclem  7275  pw1on  7293  sucpw1nel3  7300  1pi  7382  prarloclemcalc  7569  ltsopr  7663  ltsosr  7831  cnm  7899  axicn  7930  axaddf  7935  axmulf  7936  nnindnn  7960  mpomulf  8016  ltso  8104  negiso  8982  nnind  9006  0z  9337  dfuzi  9436  cnref1o  9725  elrpii  9731  xrltso  9871  0e0icopnf  10054  0e0iccpnf  10055  fz0to4untppr  10199  fldiv4p1lem1div2  10395  expcl2lemap  10643  expclzaplem  10655  expge0  10667  expge1  10668  xrnegiso  11427  fclim  11459  eff2  11845  reeff1  11865  ef01bndlem  11921  sin01bnd  11922  cos01bnd  11923  sin01gt0  11927  egt2lt3  11945  halfleoddlt  12059  2prm  12295  3prm  12296  1arith  12536  setsslnid  12730  xpsff1o  12992  isabli  13430  rngmgpf  13493  mgpf  13567  zringnzr  14158  fntopon  14260  istpsi  14275  ismeti  14582  cnfldms  14772  tgqioo  14791  addcncntoplem  14797  divcnap  14801  abscncf  14821  recncf  14822  imcncf  14823  cjcncf  14824  maxcncf  14851  mincncf  14852  dveflem  14962  reeff1o  15009  reefiso  15013  ioocosf1o  15090  lgslem2  15242  lgsfcl2  15247  lgsne0  15279  2lgslem1b  15330  ex-fl  15371  bj-indint  15577  bj-omord  15606  012of  15640  2o01f  15641  0nninf  15648  peano4nninf  15650  taupi  15717