Theorem mpbir2an 729

Description: Detach a conjunction of truths in a biconditional.

Hypotheses

Ref	Expression
mpbiran.1	|- (ph <-> (ps /\ ch))
mpbir2an.2	|- ps
mpbir2an.3	|- ch

Assertion

Ref	Expression
mpbir2an	|- ph

Proof of Theorem mpbir2an

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

Syntax hints:   <-> wb 146   /\ wa 223

This theorem is referenced by:  3pm3.2i 817  eqssi 2074  dtruALT 2743  itlso 2858  we0 2939  ordon 2982  ord0 3016  relsn 3249  cnvun 3447  funsn 3535  funi 3537  fnresi 3595  fn0 3597  f0 3647  fconst 3649  f10 3704  f1o0 3707  f1oi 3708  f1osn 3710  fopabsn 3831  fvi 3833  isoid 3886  tfrlem7 3908  tfr1 3915  tz7.44-1 3919  tz7.44-2 3920  frfnom 3942  fo1st 4081  fo2nd 4082  df1st2 4116  df2nd2 4117  oawordeulem 4178  canth2 4470  xpmapenlem5 4486  unfilem2 4531  rankpw 4664  rankuni2 4670  alephiso 4872  alephfplem4 4879  1pi 4991  1pr 5097  axaddopr 5245  axmulopr 5246  axicn 5250  negeu 5335  receu 5678  mulnzcnopr 5679  divval 5681  nnind 5893  0z 6101  elrpi 6229  om2uzuz 6242  om2uzf1o 6246  uzrdgini 6248  uzrdginip1 6250  seq1res 6272  ser1ref 6277  ser1f2 6279  seq1shftid 6301  icoshftf1oi 6350  seq1seqz 6481  seq1seq0 6485  dfseq0 6503  ser0f 6505  sqrlem6 6616  sqrlem23 6633  ref 6698  imf 6699  caure 6872  cauim 6873  ser1absdiflem 6874  serzref 6997  caucvg3a 7108  caucvg3lem 7110  ser1f0 7114  cvgcmp2lem 7124  cvgcmp2clem 7126  cvgcmp3c 7130  isumcmpi 7158  fnsmnt 7169  negfcncf 7212  ivthlem4 7227  ivthlem8 7231  ivthlem9 7232  ivthlem4OLD 7236  ivthlem8OLD 7240  eff 7263  efaddlem12 7299  eff2 7320  reeff1 7358  eflegeolem2 7362  efcn 7371  reeff1o 7376  reefiso 7378  sinf 7390  cosf 7391  qnnen 7454  ruclem8 7468  ruclem13 7473  ruc 7500  sn0top 7597  indistop 7598  distop 7599  fctop 7600  cctop 7602  retps 7608  ishausi 7735  ismsi 7751  ismeti 7752  0met 7777  metxp 7786  iscms2i 7945  isgrpi 7992  grprn 8006  isgrp2i 8026  isabliOLD 8057  isabli 8058  issubgi 8074  ablmul 8083  mulid 8084  ghgrpilem4 8088  cnring 8114  ringsn 8115  nmcnilem 8285  sm1cnilem 8294  ipcl 8312  lnocoi 8365  cnph 8422  cnbn 8472  ubthlem6 8478  minveceu 8527  cnhl 8561  htthlem12 8574  sinco 8605  cosco 8606  pilem2 8610  efif 8655  efifo 8663  efif1 8671  efif1o 8672  circgrpOLD 8677  eff1i 8683  effoi 8684  eff1oi 8685  pilog 8707  norm3adif 8954  hhip 8983  hhph 8984  hhhl 9012  hlim0 9044  hlimcaui 9045  helch 9055  hsn0elch 9059  hhssnv 9073  hhshsslem2 9077  hhssbn 9090  hhsshl 9091  occl 9120  projlem8 9132  pjpj0 9193  shscl 9219  shintcl 9231  chintcl 9233  shsumval2 9298  lejdi 9399  osumlem7 9524  nonbool 9536  pjfo 9588  pjf 9589  pjmf1 9601  df0op2 9618  idunop 9841  0cnop 9842  0cnfn 9843  idcnop 9844  idhmop 9845  0hmop 9846  0lnfn 9848  0bdop 9856  lnophs 9864  lnopco 9866  lnopco0 9867  lnopuni 9875  lnophm 9881  nmcopext 9897  nmcoplbt 9898  nmcfnext 9926  nmcfnlbt 9927  nlelsh 9931  nlelch 9932  riesz4 9934  riesz4t 9935  riesz1t 9936  cnlnadjlem6 9943  cnlnadjlem9 9946  cnlnadjeu 9948  cnlnadjeut 9949  nmopadj 9961  bdophs 9967  bdopco 9969  nmopcoadj 9972  pjhmop 10011  pjbdln 10014  hmopidmch 10017  hmopidmpj 10018  mdslj1 10183  ghomsn 10322  cayleylem2 10344  cayleylem3 10345  stcat 10389  dtt2 10498  dmse1 10503  iintlem1 10512  iintlem2 10513  stoi 10519  1alg 10534  1ded 10551  0alg 10569  0ded 10570  0cat 10571  1cat 10572

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain