Theorem mpbir2an 735

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

Syntax hints:   <-> wb 144   /\ wa 221

This theorem is referenced by:  3pm3.2i 824  eqssi 2130  dtru 2831  itlso 2942  we0 2971  ord0 3025  ordon 3141  relsn 3343  cnvun 3540  coundi 3600  coundir 3601  funsn 3648  funi 3650  fnresi 3709  fn0 3711  f0 3763  fconst 3765  f10 3824  f1o0 3827  f1oi 3828  f1osn 3830  fvi 3956  isoid 4009  fo1st 4152  fo2nd 4153  tfrlem7 4218  tfr1 4225  tz7.44-1 4229  tz7.44-2 4230  frfnom 4252  oawordeulem 4324  canth2 4629  xpmapenlem5 4647  unfilem2 4695  rankpw 4830  rankuni2 4836  alephiso 5042  alephfplem4 5049  1pi 5165  1pr 5271  axaddopr 5419  axmulopr 5420  axicn 5424  negeui 5509  receui 5853  mulnzcnopr 5854  divvali 5856  nnind 6082  elrpii 6193  0z 6314  icoshftf1oii 6536  om2uzuzi 6660  om2uzf1oi 6664  om2uzisoi 6665  uzrdginii 6667  uzrdginip1i 6669  ser1refi 6697  ser1f2i 6699  dfseq0 6758  ser0fi 6760  sqrlem6 6879  sqrlem23 6896  ref 6960  imf 6961  caurei 7130  cauimi 7131  ser1absdiflem 7132  serzrefi 7254  caucvg3ai 7367  caucvg3lem 7369  cvgcmp2lem 7383  cvgcmp2clem 7385  cvgcmp2clemOLD 7386  cvgcmp3ci 7390  isumcmpii 7419  arisumi 7430  negfcncfi 7474  ivthlem4 7489  ivthlem8 7493  ivthlem9 7494  eff 7518  efaddlem12 7554  eff2 7575  egt2OLD 7600  elt3OLD 7601  egt2lt3 7602  reeff1 7618  eflegeolem2 7622  efcn 7631  reeff1o 7634  reefiso 7636  sinf 7648  cosf 7649  qnnen 7715  ruclem8 7729  ruclem13 7734  ruc 7761  sn0top 7859  distop 7861  cctop 7862  retps 7868  ishausi 7995  ismsi 8011  ismeti 8012  0met 8035  metxp 8044  iscms2i 8206  isgrpi 8255  grprn 8269  isgrp2i 8293  isabli 8347  issubgi 8364  ablmul 8372  mulid 8373  ghgrpilem4 8377  cnring 8404  ringsn 8405  nmcnilem 8591  sm1cnilem 8601  ipcl 8619  lnocoi 8672  cnph 8734  cnbn 8786  ubthlem6 8792  minveceu 8843  cnhl 8880  htthlem12 8893  pilem2 8939  efif 8993  efifo 9001  efif1 9009  efif1o 9010  eff1i 9016  effoi 9017  eff1oi 9018  pilog 9040  norm3adifii 9291  hhip 9320  hhph 9321  hhhl 9349  hlim0 9381  hlimcauii 9382  helch 9392  hsn0elch 9396  hhssnv 9410  hhshsslem2 9414  hhssbn 9427  hhsshl 9428  occli 9457  projlem8 9469  projlemHIL 9494  pjpj0i 9531  shscli 9557  shintcli 9569  chintcli 9571  shsumval2i 9636  lejdii 9737  osumlem7 9862  nonbooli 9874  pjfoi 9926  pjfi 9927  pjmf1 9939  df0op2 9958  idunop 10181  0cnop 10182  0cnfn 10183  idcnop 10184  idhmop 10185  0hmop 10186  0lnfn 10188  0bdop 10197  lnophsi 10205  lnopcoi 10207  lnopunii 10216  lnophmi 10222  nmcopex 10238  nmcoplb 10239  nmcfnex 10267  nmcfnlb 10268  nlelshi 10272  nlelchi 10273  riesz4i 10275  riesz4 10276  riesz1 10277  cnlnadjlem6 10284  cnlnadjlem9 10287  cnlnadjeui 10289  cnlnadjeu 10290  nmopadji 10302  bdophsi 10308  bdopcoi 10310  nmopcoadji 10313  pjhmopi 10353  pjbdlni 10356  hmopidmchi 10359  mdslj1i 10527  ghomsn 10673  cayleylem2 10695  cayleylem3 10696  stcat 10741  vxveqv 10761  prj1 10809  zrdivrng 10969  stoiglem 11063  dtt2 11110  sinempcomp 11116  indcomp 11118  intopcon 11133  stoi 11145  1alg 11176  1ded 11192  0alg 11210  0ded 11211  0cat 11212  1cat 11213  compfipin0lem 11492  alexsublem2 11497  alexsublem4 11499  comppfsc 11578  ga0 11775  absrdbnd 11870  mettrifi 11912  heiborlem18 12028  heiborlem21 12031  heiborlem29 12039  heiborlem35 12045  bfplem10 12063  recms 12066  ismrer1 12080  phtpycolem3 12095  phtpycolem4 12096

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 145  df-an 223

Copyright terms: Public domain