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  11515  fclim  11547  eff2  11933  reeff1  11953  ef01bndlem  12009  sin01bnd  12010  cos01bnd  12011  sin01gt0  12015  egt2lt3  12033  halfleoddlt  12147  2prm  12391  3prm  12392  1arith  12632  setsslnid  12826  xpsff1o  13123  isabli  13578  rngmgpf  13641  mgpf  13715  zringnzr  14306  fntopon  14438  istpsi  14453  ismeti  14760  cnfldms  14950  tgqioo  14969  addcncntoplem  14975  divcnap  14979  abscncf  14999  recncf  15000  imcncf  15001  cjcncf  15002  maxcncf  15029  mincncf  15030  dveflem  15140  reeff1o  15187  reefiso  15191  ioocosf1o  15268  lgslem2  15420  lgsfcl2  15425  lgsne0  15457  2lgslem1b  15508  ex-fl  15594  bj-indint  15800  bj-omord  15829  012of  15863  2o01f  15864  0nninf  15874  peano4nninf  15876  taupi  15945