Theorem mpbir2an 800

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

Syntax hints:   <-> wb 163   /\ wa 240

This theorem is referenced by:  3pm3.2i 1048  eqssi 2632  dtru 3498  itlso 3619  so0 3621  we0 3653  ord0 3715  ordon 3863  omssnlim 3965  relsn 4087  cnvunOLD 4323  coundiOLD 4397  coundirOLD 4399  funi 4452  funsn 4463  funsnOLD 4464  fnsn 4469  fnresi 4529  fn0 4532  fn0OLD 4533  f0 4600  fconst 4602  fconstOLD 4603  f10 4667  f1o0 4670  f1oi 4671  f1oiOLD 4672  f1osn 4674  f1osnOLD 4675  fvi 4818  isoid 4872  fo1st 5032  fo2nd 5033  tfrlem7 5125  tfr1 5132  tz7.44-1 5136  tz7.44-2 5137  frfnom 5159  oawordeulem 5236  canth2 5548  xpmapenlem5 5594  unfilem2 5642  rankpw 5795  rankuni2 5801  alephiso 6040  alephfplem4 6047  1pi 6163  1pr 6269  axaddopr 6417  axmulopr 6418  axicn 6423  negeui 6510  receui 6890  mulnzcnopr 6891  divvali 6893  nnind 7120  elrpii 7234  0z 7355  icoshftf1oii 7578  om2uzuzi 7708  om2uzf1oi 7712  om2uzisoi 7713  uzrdginii 7715  uzrdginip1i 7717  ser1refi 7745  ser1f2i 7747  dfseq0 7806  ser0fi 7808  sqrlem6 7928  sqrlem23 7945  ref 8009  imf 8010  caurei 8179  cauimi 8180  ser1absdiflem 8181  serzrefi 8311  caucvg3ai 8424  caucvg3lem 8426  cvgcmp2lem 8440  cvgcmp2clem 8442  cvgcmp2clemOLD 8443  cvgcmp3ci 8447  isumcmpii 8476  arisumi 8487  negfcncfi 8531  ivthlem4 8546  ivthlem8 8550  ivthlem9 8551  eff 8575  efaddlem12 8611  eff2 8632  egt2OLD 8657  elt3OLD 8658  egt2lt3 8659  reeff1 8675  eflegeolem2 8679  efcn 8688  reeff1o 8691  reefiso 8693  sinf 8705  cosf 8706  qnnen 8772  ruclem8 8786  ruclem13 8791  ruc 8818  sn0top 8917  distop 8919  fctop 8920  cctop 8922  retps 8928  ishausi 9062  ismsi 9078  ismeti 9079  0met 9102  metxp 9111  iscms2i 9273  isgrpi 9322  grprn 9336  isgrp2i 9360  isabli 9414  issubgi 9431  ablmul 9439  mulid 9440  ghgrpilem4 9444  ga0 9453  cnring 9489  ringsn 9490  nmcnilem 9676  sm1cnilem 9686  ipcl 9704  lnocoi 9757  cnph 9819  cnbn 9871  ubthlem6 9877  minveceu 9928  cnhl 9965  htthlem12 9978  pilem2 10021  efif 10075  efifo 10083  efif1 10091  efif1o 10092  eff1i 10098  effoi 10099  eff1oi 10100  pilog 10122  stoiglem 10250  zrdivrng 10418  norm3adifii 10648  hhip 10677  hhph 10678  hhhl 10706  hlim0 10738  hlimcauii 10739  helch 10749  hsn0elch 10753  hhssnv 10767  hhshsslem2 10771  hhssbn 10784  hhsshl 10785  occli 10814  projlem8 10826  projlemHIL 10851  pjpj0i 10888  shscli 10914  shintcli 10926  chintcli 10928  shsumval2i 10993  lejdii 11094  osumlem7 11219  nonbooli 11231  pjfoi 11283  pjfi 11284  pjmf1 11296  df0op2 11315  idunop 11539  0cnop 11540  0cnfn 11541  idcnop 11542  idhmop 11543  0hmop 11544  0lnfn 11546  0bdop 11555  lnophsi 11563  lnopcoi 11565  lnopunii 11574  lnophmi 11580  nmcopex 11596  nmcoplb 11597  nmcfnex 11625  nmcfnlb 11626  nlelshi 11630  nlelchi 11631  riesz4i 11633  riesz4 11634  riesz1 11635  cnlnadjlem6 11642  cnlnadjlem9 11645  cnlnadjeui 11647  cnlnadjeu 11648  nmopadji 11660  bdophsi 11666  bdopcoi 11668  nmopcoadji 11671  pjhmopi 11717  pjbdlni 11720  hmopidmchi 11723  mdslj1i 11891  bnj107 12452  ghomsn 13631  cayleylem2 13642  cayleylem3 13643  divalglem9 13704  gcdf 13725  eucalgf 13751  soxp 13950  wexp 13952  soseq 13955  wfrlem11 13967  wfr1 13973  axbday 14012  bdayfn 14016  brsset 14069  brbigcup 14074  fnbigcup 14075  stcat 14347  vxveqv 14357  prj1 14395  symgfo 14730  zintdom 14787  dtt2 14951  sinempcomp 14953  indcomp 14955  intopcon 14964  stoi 14998  cntrsetlem 14999  1alg 15069  1ded 15085  0alg 15103  0ded 15104  0cat 15105  1cat 15106  compfipin0lem 15435  alexsublem2 15438  alexsublem4 15440  comppfsc 15517  absrdbnd 15799  mettrifi 15847  heiborlem18 15972  heiborlem21 15975  heiborlem29 15983  heiborlem35 15989  bfplem10 16007  recms 16010  ismrer1 16024  phtpycolem3 16053  phtpycolem4 16054  pcohtpylem3 16082  iordsmo 16448  stb2xpl 16742  islati 16854  isclati 16892  isolati 16943  isomli 16960  isatlati 17015  ishlati 17019  isabliNEW 17136

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 164  df-an 242

Copyright terms: Public domain