Theorem mpbir2an 955

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

This proof depends on syntax axioms:   ∧ wa 104   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  3pm3.2i  1206  euequ1  2182  eqssi  3264  elini  3413  dtruarb  4330  opnzi  4377  so0  4473  we0  4508  ord0  4538  ordon  4635  onsucelsucexmidlem1  4677  regexmidlemm  4681  ordpwsucexmid  4719  reg3exmidlemwe  4728  ordom  4756  funi  5412  funcnvsn  5429  funinsn  5433  fnresi  5504  fn0  5506  f0  5586  fconst  5591  f10  5677  f1o0  5681  f1oi  5682  f1osn  5684  funopsn  5894  isoid  6019  iso0  6026  rinvf1o  6038  acexmidlem2  6085  fo1st  6395  fo2nd  6396  iordsmo  6572  tfrlem7  6592  tfrexlem  6609  mapsnf1o2  6983  1domsn  7120  inresflem  7407  0ct  7454  infnninf  7471  infnninfOLD  7472  exmidonfinlem  7552  exmidaclem  7571  pw1on  7592  sucpw1nel3  7599  1pi  7689  prarloclemcalc  7876  ltsopr  7970  ltsosr  8138  cnm  8206  axicn  8237  axaddf  8242  axmulf  8243  nnindnn  8267  mpomulf  8323  ltso  8410  negiso  9294  nnind  9330  0z  9667  dfuzi  9768  cnref1o  10069  elrpii  10075  xrltso  10216  0e0icopnf  10399  0e0iccpnf  10400  fz0to4untppr  10549  fldiv4p1lem1div2  10762  expcl2lemap  11010  expclzaplem  11022  expge0  11034  expge1  11035  xrnegiso  12054  fclim  12086  eff2  12473  reeff1  12493  ef01bndlem  12549  sin01bnd  12550  cos01bnd  12551  sin01gt0  12555  egt2lt3  12573  halfleoddlt  12687  2prm  12931  3prm  12932  1arith  13176  prmlem1a  13251  ballotfilemonn  13280  ballotfilem2  13287  setsslnid  13463  xpsff1o  13730  isabli  14194  rngmgpf  14344  mgpf  14423  zringnzr  15047  fntopon  15262  istpsi  15277  ismeti  15584  cnfldms  15774  tgqioo  15793  addcncntoplem  15799  divcnap  15803  abscncf  15823  recncf  15824  imcncf  15825  cjcncf  15826  maxcncf  15853  mincncf  15854  dveflem  15964  reeff1o  16011  reefiso  16015  ioocosf1o  16094  efnnfsumcl  16251  efchtqdvds  16277  ppiqub  16305  lgslem2  16337  lgsfcl2  16342  lgsne0  16374  2lgslem1b  16425  umgrbien  16568  konigsberglem1  16946  konigsberglem4  16949  ex-fl  16956  bj-indint  17174  bj-omord  17203  012of  17240  2o01f  17241  0nninf  17265  peano4nninf  17267  taupi  17342