Theorem mpbir2an 948

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 946	. 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  1199  euequ1  2173  eqssi  3240  elini  3388  dtruarb  4276  opnzi  4322  so0  4418  we0  4453  ord0  4483  ordon  4579  onsucelsucexmidlem1  4621  regexmidlemm  4625  ordpwsucexmid  4663  reg3exmidlemwe  4672  ordom  4700  funi  5353  funcnvsn  5369  funinsn  5373  fnresi  5444  fn0  5446  f0  5521  fconst  5526  f10  5611  f1o0  5615  f1oi  5616  f1osn  5618  funopsn  5822  isoid  5943  iso0  5950  acexmidlem2  6007  fo1st  6312  fo2nd  6313  iordsmo  6454  tfrlem7  6474  tfrexlem  6491  mapsnf1o2  6856  1domsn  6989  inresflem  7243  0ct  7290  infnninf  7307  infnninfOLD  7308  exmidonfinlem  7387  exmidaclem  7406  pw1on  7427  sucpw1nel3  7434  1pi  7518  prarloclemcalc  7705  ltsopr  7799  ltsosr  7967  cnm  8035  axicn  8066  axaddf  8071  axmulf  8072  nnindnn  8096  mpomulf  8152  ltso  8240  negiso  9118  nnind  9142  0z  9473  dfuzi  9573  cnref1o  9863  elrpii  9869  xrltso  10009  0e0icopnf  10192  0e0iccpnf  10193  fz0to4untppr  10337  fldiv4p1lem1div2  10542  expcl2lemap  10790  expclzaplem  10802  expge0  10814  expge1  10815  xrnegiso  11794  fclim  11826  eff2  12212  reeff1  12232  ef01bndlem  12288  sin01bnd  12289  cos01bnd  12290  sin01gt0  12294  egt2lt3  12312  halfleoddlt  12426  2prm  12670  3prm  12671  1arith  12911  setsslnid  13105  xpsff1o  13403  isabli  13858  rngmgpf  13921  mgpf  13995  zringnzr  14587  fntopon  14719  istpsi  14734  ismeti  15041  cnfldms  15231  tgqioo  15250  addcncntoplem  15256  divcnap  15260  abscncf  15280  recncf  15281  imcncf  15282  cjcncf  15283  maxcncf  15310  mincncf  15311  dveflem  15421  reeff1o  15468  reefiso  15472  ioocosf1o  15549  lgslem2  15701  lgsfcl2  15706  lgsne0  15738  2lgslem1b  15789  umgrbien  15931  ex-fl  16198  bj-indint  16403  bj-omord  16432  012of  16470  2o01f  16471  0nninf  16484  peano4nninf  16486  taupi  16555