Theorem mpbir2an 945

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 943	. 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  1178  euequ1  2150  eqssi  3213  elini  3361  dtruarb  4243  opnzi  4287  so0  4381  we0  4416  ord0  4446  ordon  4542  onsucelsucexmidlem1  4584  regexmidlemm  4588  ordpwsucexmid  4626  reg3exmidlemwe  4635  ordom  4663  funi  5312  funcnvsn  5328  funinsn  5332  fnresi  5403  fn0  5405  f0  5478  fconst  5483  f10  5568  f1o0  5572  f1oi  5573  f1osn  5575  funopsn  5775  isoid  5892  iso0  5899  acexmidlem2  5954  fo1st  6256  fo2nd  6257  iordsmo  6396  tfrlem7  6416  tfrexlem  6433  mapsnf1o2  6796  1domsn  6929  inresflem  7177  0ct  7224  infnninf  7241  infnninfOLD  7242  exmidonfinlem  7317  exmidaclem  7336  pw1on  7357  sucpw1nel3  7364  1pi  7448  prarloclemcalc  7635  ltsopr  7729  ltsosr  7897  cnm  7965  axicn  7996  axaddf  8001  axmulf  8002  nnindnn  8026  mpomulf  8082  ltso  8170  negiso  9048  nnind  9072  0z  9403  dfuzi  9503  cnref1o  9792  elrpii  9798  xrltso  9938  0e0icopnf  10121  0e0iccpnf  10122  fz0to4untppr  10266  fldiv4p1lem1div2  10470  expcl2lemap  10718  expclzaplem  10730  expge0  10742  expge1  10743  xrnegiso  11648  fclim  11680  eff2  12066  reeff1  12086  ef01bndlem  12142  sin01bnd  12143  cos01bnd  12144  sin01gt0  12148  egt2lt3  12166  halfleoddlt  12280  2prm  12524  3prm  12525  1arith  12765  setsslnid  12959  xpsff1o  13256  isabli  13711  rngmgpf  13774  mgpf  13848  zringnzr  14439  fntopon  14571  istpsi  14586  ismeti  14893  cnfldms  15083  tgqioo  15102  addcncntoplem  15108  divcnap  15112  abscncf  15132  recncf  15133  imcncf  15134  cjcncf  15135  maxcncf  15162  mincncf  15163  dveflem  15273  reeff1o  15320  reefiso  15324  ioocosf1o  15401  lgslem2  15553  lgsfcl2  15558  lgsne0  15590  2lgslem1b  15641  umgrbien  15781  ex-fl  15800  bj-indint  16005  bj-omord  16034  012of  16069  2o01f  16070  0nninf  16082  peano4nninf  16084  taupi  16153