Theorem mpbir2an 937

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

Syntax hints:   ∧ wa 103   ↔ wb 104

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3pm3.2i  1170  euequ1  2114  eqssi  3163  elini  3311  dtruarb  4177  opnzi  4220  so0  4311  we0  4346  ord0  4376  ordon  4470  onsucelsucexmidlem1  4512  regexmidlemm  4516  ordpwsucexmid  4554  reg3exmidlemwe  4563  ordom  4591  funi  5230  funcnvsn  5243  funinsn  5247  fnresi  5315  fn0  5317  f0  5388  fconst  5393  f10  5476  f1o0  5479  f1oi  5480  f1osn  5482  isoid  5789  iso0  5796  acexmidlem2  5850  fo1st  6136  fo2nd  6137  iordsmo  6276  tfrlem7  6296  tfrexlem  6313  mapsnf1o2  6674  1domsn  6797  inresflem  7037  0ct  7084  infnninf  7100  infnninfOLD  7101  exmidonfinlem  7170  exmidaclem  7185  pw1on  7203  sucpw1nel3  7210  1pi  7277  prarloclemcalc  7464  ltsopr  7558  ltsosr  7726  cnm  7794  axicn  7825  axaddf  7830  axmulf  7831  nnindnn  7855  ltso  7997  negiso  8871  nnind  8894  0z  9223  dfuzi  9322  cnref1o  9609  elrpii  9613  xrltso  9753  0e0icopnf  9936  0e0iccpnf  9937  fz0to4untppr  10080  fldiv4p1lem1div2  10261  expcl2lemap  10488  expclzaplem  10500  expge0  10512  expge1  10513  xrnegiso  11225  fclim  11257  eff2  11643  reeff1  11663  ef01bndlem  11719  sin01bnd  11720  cos01bnd  11721  sin01gt0  11724  egt2lt3  11742  halfleoddlt  11853  2prm  12081  3prm  12082  1arith  12319  setsslnid  12467  fntopon  12816  istpsi  12831  ismeti  13140  tgqioo  13341  addcncntoplem  13345  divcnap  13349  abscncf  13366  recncf  13367  imcncf  13368  cjcncf  13369  dveflem  13481  reeff1o  13488  reefiso  13492  ioocosf1o  13569  lgslem2  13696  lgsfcl2  13701  lgsne0  13733  ex-fl  13760  bj-indint  13966  bj-omord  13995  012of  14028  2o01f  14029  0nninf  14037  peano4nninf  14039  taupi  14102