Theorem mpbir2an 883

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 881	. 2 ⊢ (𝜑 ↔ 𝜒)
5	1, 4	mpbir 144	1 ⊢ 𝜑

Syntax hints:   ∧ wa 102   ↔ wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  3pm3.2i  1116  euequ1  2036  eqssi  3015  dtruarb  3962  opnzi  3990  so0  4081  we0  4116  ord0  4146  ordon  4230  onsucelsucexmidlem1  4271  regexmidlemm  4275  ordpwsucexmid  4313  reg3exmidlemwe  4321  ordom  4347  funi  4952  funcnvsn  4965  fnresi  5036  fn0  5038  f0  5100  fconst  5102  f10  5180  f1o0  5183  f1oi  5184  f1osn  5186  isoid  5470  acexmidlem2  5529  fo1st  5804  fo2nd  5805  iordsmo  5935  tfrlem7  5956  tfrexlem  5971  1pi  6505  prarloclemcalc  6692  ltsopr  6786  ltsosr  6941  axicn  7031  nnindnn  7059  ltso  7189  negiso  8033  nnind  8055  0z  8362  dfuzi  8457  cnref1o  8733  elrpii  8737  xrltso  8871  0e0icopnf  9002  0e0iccpnf  9003  fldiv4p1lem1div2  9307  expcl2lemap  9488  expclzaplem  9500  expge0  9512  expge1  9513  fclim  10133  halfleoddlt  10294  2prm  10509  3prm  10510  ex-fl  10563  bj-indint  10726  bj-omord  10755