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	|- ps
mpbir2an.2	|- ch
mpbiran2an.1	|- ( ph <-> ( ps /\ ch ) )

Assertion

Ref	Expression
mpbir2an	|- ph

Proof of Theorem mpbir2an

Step	Hyp	Ref	Expression
1		mpbir2an.2	. 2 |- ch
2		mpbir2an.1	. . 3 |- ps
3		mpbiran2an.1	. . 3 |- ( ph <-> ( ps /\ ch ) )
4	2, 3	mpbiran 942	. 2 |- ( ph <-> ch )
5	1, 4	mpbir 146	1 |- ph

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  2148  eqssi  3208  elini  3356  dtruarb  4234  opnzi  4278  so0  4372  we0  4407  ord0  4437  ordon  4533  onsucelsucexmidlem1  4575  regexmidlemm  4579  ordpwsucexmid  4617  reg3exmidlemwe  4626  ordom  4654  funi  5302  funcnvsn  5318  funinsn  5322  fnresi  5392  fn0  5394  f0  5465  fconst  5470  f10  5555  f1o0  5558  f1oi  5559  f1osn  5561  funopsn  5761  isoid  5878  iso0  5885  acexmidlem2  5940  fo1st  6242  fo2nd  6243  iordsmo  6382  tfrlem7  6402  tfrexlem  6419  mapsnf1o2  6782  1domsn  6913  inresflem  7161  0ct  7208  infnninf  7225  infnninfOLD  7226  exmidonfinlem  7300  exmidaclem  7319  pw1on  7337  sucpw1nel3  7344  1pi  7427  prarloclemcalc  7614  ltsopr  7708  ltsosr  7876  cnm  7944  axicn  7975  axaddf  7980  axmulf  7981  nnindnn  8005  mpomulf  8061  ltso  8149  negiso  9027  nnind  9051  0z  9382  dfuzi  9482  cnref1o  9771  elrpii  9777  xrltso  9917  0e0icopnf  10100  0e0iccpnf  10101  fz0to4untppr  10245  fldiv4p1lem1div2  10446  expcl2lemap  10694  expclzaplem  10706  expge0  10718  expge1  10719  xrnegiso  11544  fclim  11576  eff2  11962  reeff1  11982  ef01bndlem  12038  sin01bnd  12039  cos01bnd  12040  sin01gt0  12044  egt2lt3  12062  halfleoddlt  12176  2prm  12420  3prm  12421  1arith  12661  setsslnid  12855  xpsff1o  13152  isabli  13607  rngmgpf  13670  mgpf  13744  zringnzr  14335  fntopon  14467  istpsi  14482  ismeti  14789  cnfldms  14979  tgqioo  14998  addcncntoplem  15004  divcnap  15008  abscncf  15028  recncf  15029  imcncf  15030  cjcncf  15031  maxcncf  15058  mincncf  15059  dveflem  15169  reeff1o  15216  reefiso  15220  ioocosf1o  15297  lgslem2  15449  lgsfcl2  15454  lgsne0  15486  2lgslem1b  15537  ex-fl  15623  bj-indint  15829  bj-omord  15858  012of  15892  2o01f  15893  0nninf  15903  peano4nninf  15905  taupi  15974