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	|- 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 953	. 2 |- ( ph <-> ch )
5	1, 4	mpbir 146	1 |- ph

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  4328  opnzi  4375  so0  4471  we0  4506  ord0  4536  ordon  4633  onsucelsucexmidlem1  4675  regexmidlemm  4679  ordpwsucexmid  4717  reg3exmidlemwe  4726  ordom  4754  funi  5409  funcnvsn  5426  funinsn  5430  fnresi  5501  fn0  5503  f0  5583  fconst  5588  f10  5674  f1o0  5678  f1oi  5679  f1osn  5681  funopsn  5891  isoid  6016  iso0  6023  rinvf1o  6035  acexmidlem2  6082  fo1st  6391  fo2nd  6392  iordsmo  6568  tfrlem7  6588  tfrexlem  6605  mapsnf1o2  6978  1domsn  7115  inresflem  7401  0ct  7448  infnninf  7465  infnninfOLD  7466  exmidonfinlem  7546  exmidaclem  7565  pw1on  7586  sucpw1nel3  7593  1pi  7683  prarloclemcalc  7870  ltsopr  7964  ltsosr  8132  cnm  8200  axicn  8231  axaddf  8236  axmulf  8237  nnindnn  8261  mpomulf  8317  ltso  8404  negiso  9288  nnind  9323  0z  9660  dfuzi  9761  cnref1o  10062  elrpii  10068  xrltso  10209  0e0icopnf  10392  0e0iccpnf  10393  fz0to4untppr  10542  fldiv4p1lem1div2  10755  expcl2lemap  11003  expclzaplem  11015  expge0  11027  expge1  11028  xrnegiso  12047  fclim  12079  eff2  12466  reeff1  12486  ef01bndlem  12542  sin01bnd  12543  cos01bnd  12544  sin01gt0  12548  egt2lt3  12566  halfleoddlt  12680  2prm  12924  3prm  12925  1arith  13169  prmlem1a  13244  ballotfilemonn  13273  ballotfilem2  13280  setsslnid  13456  xpsff1o  13723  isabli  14187  rngmgpf  14320  mgpf  14399  zringnzr  15021  fntopon  15216  istpsi  15231  ismeti  15538  cnfldms  15728  tgqioo  15747  addcncntoplem  15753  divcnap  15757  abscncf  15777  recncf  15778  imcncf  15779  cjcncf  15780  maxcncf  15807  mincncf  15808  dveflem  15918  reeff1o  15965  reefiso  15969  ioocosf1o  16047  efnnfsumcl  16200  efchtqdvds  16226  ppiqub  16254  lgslem2  16286  lgsfcl2  16291  lgsne0  16323  2lgslem1b  16374  umgrbien  16517  konigsberglem1  16895  konigsberglem4  16898  ex-fl  16905  bj-indint  17123  bj-omord  17152  012of  17189  2o01f  17190  0nninf  17213  peano4nninf  17215  taupi  17290