Theorem mpbir2an 728

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

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

This theorem is referenced by:  3pm3.2i 816  eqssi 2068  dtruALT 2738  itlso 2854  we0 2934  ordon 2977  ord0 3011  relsn 3244  cnvun 3441  funsn 3529  funi 3531  fnresi 3589  fn0 3591  f0 3641  fconst 3643  f10 3698  f1o0 3701  f1oi 3702  f1osn 3704  fopabsn 3825  fvi 3827  isoid 3880  tfrlem7 3902  tfr1 3909  tz7.44-1 3913  tz7.44-2 3914  frfnom 3936  fo1st 4075  fo2nd 4076  df1st2 4110  df2nd2 4111  oawordeulem 4172  canth2 4464  xpmapenlem5 4480  unfilem2 4525  rankpw 4656  rankuni2 4662  alephiso 4864  alephfplem4 4871  1pi 4983  1pr 5089  axaddopr 5237  axmulopr 5238  axicn 5242  negeu 5327  receu 5670  mulnzcnopr 5671  divval 5673  nnind 5885  0z 6093  elrpi 6221  om2uzuz 6234  om2uzf1o 6238  uzrdgini 6240  uzrdginip1 6242  seq1res 6264  ser1ref 6269  ser1f2 6271  seq1shftid 6293  icoshftf1oi 6342  seq1seqz 6473  seq1seq0 6477  dfseq0 6495  ser0f 6497  sqrlem6 6608  sqrlem23 6625  ref 6690  imf 6691  caure 6864  cauim 6865  ser1absdiflem 6866  serzref 6989  caucvg3a 7100  caucvg3lem 7102  ser1f0 7106  cvgcmp2lem 7116  cvgcmp2clem 7118  cvgcmp3c 7122  isumcmpi 7150  fnsmnt 7161  negfcncf 7204  ivthlem4 7219  ivthlem8 7223  ivthlem9 7224  ivthlem4OLD 7228  ivthlem8OLD 7232  eff 7255  efaddlem12 7291  eff2 7312  reeff1 7350  eflegeolem2 7354  efcn 7363  reeff1o 7368  reefiso 7370  sinf 7382  cosf 7383  qnnen 7446  ruclem8 7460  ruclem13 7465  ruc 7492  sn0top 7589  indistop 7590  distop 7591  fctop 7592  cctop 7594  retps 7600  ishausi 7724  ismsi 7740  ismeti 7741  0met 7765  metxp 7774  iscms2i 7929  isgrpi 7976  grprn 7990  isgrp2i 8011  isabliOLD 8042  isabli 8043  issubgi 8059  ablmul 8068  mulid 8069  ghgrpilem4 8073  cnring 8099  ringsn 8100  nmcnilem 8272  sm1cnilem 8281  ipcl 8299  lnocoi 8352  cnph 8409  cnbn 8459  ubthlem6 8465  minveceu 8514  cnhl 8548  htthlem12 8561  sinco 8586  cosco 8587  pilem2 8591  efif 8636  efifo 8644  efif1 8652  efif1o 8653  circgrpOLD 8658  eff1i 8665  effoi 8666  effoiOLD 8667  eff1oi 8668  pilog 8690  norm3adif 8936  hhip 8965  hhph 8966  hhhl 8994  hlim0 9026  hlimcaui 9027  helch 9037  hsn0elch 9041  hhssnv 9054  hhshsslem2 9058  hhssbn 9068  occl 9097  projlem8 9109  pjpj0 9170  shscl 9196  shintcl 9208  chintcl 9210  shsumval2 9275  lejdi 9376  osumlem7 9501  nonbool 9513  pjfo 9565  pjf 9566  pjmf1 9578  df0op2 9595  idunop 9818  0cnop 9819  0cnfn 9820  idcnop 9821  idhmop 9822  0hmop 9823  0lnfn 9825  0bdop 9833  lnophs 9841  lnopco 9843  lnopco0 9844  lnopuni 9852  lnophm 9858  nmcopext 9874  nmcoplbt 9875  nmcfnext 9903  nmcfnlbt 9904  nlelsh 9908  nlelch 9909  riesz4 9911  riesz4t 9912  riesz1t 9913  cnlnadjlem6 9920  cnlnadjlem9 9923  cnlnadjeu 9925  cnlnadjeut 9926  nmopadj 9938  bdophs 9943  bdopco 9945  nmopcoadj 9948  pjhmop 9984  pjbdln 9987  hmopidmch 9990  hmopidmpj 9991  mdslj1 10154  ghomsn 10293  cayleylem2 10317  cayleylem3 10318  stcat 10353  dtt2 10462  dmse1 10467  iintlem1 10476  iintlem2 10477  stoi 10483  1alg 10498  1ded 10515  0alg 10533  0ded 10534  0cat 10535  1cat 10536

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