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  2119  eqssi  3169  elini  3317  dtruarb  4186  opnzi  4229  so0  4320  we0  4355  ord0  4385  ordon  4479  onsucelsucexmidlem1  4521  regexmidlemm  4525  ordpwsucexmid  4563  reg3exmidlemwe  4572  ordom  4600  funi  5240  funcnvsn  5253  funinsn  5257  fnresi  5325  fn0  5327  f0  5398  fconst  5403  f10  5487  f1o0  5490  f1oi  5491  f1osn  5493  isoid  5801  iso0  5808  acexmidlem2  5862  fo1st  6148  fo2nd  6149  iordsmo  6288  tfrlem7  6308  tfrexlem  6325  mapsnf1o2  6686  1domsn  6809  inresflem  7049  0ct  7096  infnninf  7112  infnninfOLD  7113  exmidonfinlem  7182  exmidaclem  7197  pw1on  7215  sucpw1nel3  7222  1pi  7289  prarloclemcalc  7476  ltsopr  7570  ltsosr  7738  cnm  7806  axicn  7837  axaddf  7842  axmulf  7843  nnindnn  7867  ltso  8009  negiso  8885  nnind  8908  0z  9237  dfuzi  9336  cnref1o  9623  elrpii  9627  xrltso  9767  0e0icopnf  9950  0e0iccpnf  9951  fz0to4untppr  10094  fldiv4p1lem1div2  10275  expcl2lemap  10502  expclzaplem  10514  expge0  10526  expge1  10527  xrnegiso  11238  fclim  11270  eff2  11656  reeff1  11676  ef01bndlem  11732  sin01bnd  11733  cos01bnd  11734  sin01gt0  11737  egt2lt3  11755  halfleoddlt  11866  2prm  12094  3prm  12095  1arith  12332  setsslnid  12480  isabli  12911  mgpf  13000  fntopon  13102  istpsi  13117  ismeti  13426  tgqioo  13627  addcncntoplem  13631  divcnap  13635  abscncf  13652  recncf  13653  imcncf  13654  cjcncf  13655  dveflem  13767  reeff1o  13774  reefiso  13778  ioocosf1o  13855  lgslem2  13982  lgsfcl2  13987  lgsne0  14019  ex-fl  14046  bj-indint  14252  bj-omord  14281  012of  14314  2o01f  14315  0nninf  14323  peano4nninf  14325  taupi  14388