Theorem mpbir2an 942

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 940	. 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  1175  euequ1  2121  eqssi  3172  elini  3320  dtruarb  4192  opnzi  4236  so0  4327  we0  4362  ord0  4392  ordon  4486  onsucelsucexmidlem1  4528  regexmidlemm  4532  ordpwsucexmid  4570  reg3exmidlemwe  4579  ordom  4607  funi  5249  funcnvsn  5262  funinsn  5266  fnresi  5334  fn0  5336  f0  5407  fconst  5412  f10  5496  f1o0  5499  f1oi  5500  f1osn  5502  isoid  5811  iso0  5818  acexmidlem2  5872  fo1st  6158  fo2nd  6159  iordsmo  6298  tfrlem7  6318  tfrexlem  6335  mapsnf1o2  6696  1domsn  6819  inresflem  7059  0ct  7106  infnninf  7122  infnninfOLD  7123  exmidonfinlem  7192  exmidaclem  7207  pw1on  7225  sucpw1nel3  7232  1pi  7314  prarloclemcalc  7501  ltsopr  7595  ltsosr  7763  cnm  7831  axicn  7862  axaddf  7867  axmulf  7868  nnindnn  7892  ltso  8035  negiso  8912  nnind  8935  0z  9264  dfuzi  9363  cnref1o  9650  elrpii  9656  xrltso  9796  0e0icopnf  9979  0e0iccpnf  9980  fz0to4untppr  10124  fldiv4p1lem1div2  10305  expcl2lemap  10532  expclzaplem  10544  expge0  10556  expge1  10557  xrnegiso  11270  fclim  11302  eff2  11688  reeff1  11708  ef01bndlem  11764  sin01bnd  11765  cos01bnd  11766  sin01gt0  11769  egt2lt3  11787  halfleoddlt  11899  2prm  12127  3prm  12128  1arith  12365  setsslnid  12514  xpsff1o  12768  isabli  13103  mgpf  13194  zringnzr  13495  fntopon  13527  istpsi  13542  ismeti  13849  tgqioo  14050  addcncntoplem  14054  divcnap  14058  abscncf  14075  recncf  14076  imcncf  14077  cjcncf  14078  dveflem  14190  reeff1o  14197  reefiso  14201  ioocosf1o  14278  lgslem2  14405  lgsfcl2  14410  lgsne0  14442  ex-fl  14480  bj-indint  14686  bj-omord  14715  012of  14748  2o01f  14749  0nninf  14756  peano4nninf  14758  taupi  14823