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  2133  eqssi  3186  elini  3334  dtruarb  4209  opnzi  4253  so0  4344  we0  4379  ord0  4409  ordon  4503  onsucelsucexmidlem1  4545  regexmidlemm  4549  ordpwsucexmid  4587  reg3exmidlemwe  4596  ordom  4624  funi  5267  funcnvsn  5280  funinsn  5284  fnresi  5352  fn0  5354  f0  5425  fconst  5430  f10  5514  f1o0  5517  f1oi  5518  f1osn  5520  isoid  5832  iso0  5839  acexmidlem2  5894  fo1st  6183  fo2nd  6184  iordsmo  6323  tfrlem7  6343  tfrexlem  6360  mapsnf1o2  6723  1domsn  6846  inresflem  7090  0ct  7137  infnninf  7153  infnninfOLD  7154  exmidonfinlem  7223  exmidaclem  7238  pw1on  7256  sucpw1nel3  7263  1pi  7345  prarloclemcalc  7532  ltsopr  7626  ltsosr  7794  cnm  7862  axicn  7893  axaddf  7898  axmulf  7899  nnindnn  7923  ltso  8066  negiso  8943  nnind  8966  0z  9295  dfuzi  9394  cnref1o  9682  elrpii  9688  xrltso  9828  0e0icopnf  10011  0e0iccpnf  10012  fz0to4untppr  10156  fldiv4p1lem1div2  10338  expcl2lemap  10566  expclzaplem  10578  expge0  10590  expge1  10591  xrnegiso  11305  fclim  11337  eff2  11723  reeff1  11743  ef01bndlem  11799  sin01bnd  11800  cos01bnd  11801  sin01gt0  11804  egt2lt3  11822  halfleoddlt  11934  2prm  12162  3prm  12163  1arith  12402  setsslnid  12567  xpsff1o  12828  isabli  13256  rngmgpf  13308  mgpf  13382  zringnzr  13918  fntopon  14001  istpsi  14016  ismeti  14323  tgqioo  14524  addcncntoplem  14528  divcnap  14532  abscncf  14549  recncf  14550  imcncf  14551  cjcncf  14552  dveflem  14664  reeff1o  14671  reefiso  14675  ioocosf1o  14752  lgslem2  14880  lgsfcl2  14885  lgsne0  14917  ex-fl  14955  bj-indint  15161  bj-omord  15190  012of  15224  2o01f  15225  0nninf  15232  peano4nninf  15234  taupi  15300