Theorem mpbir2an 730

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

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

This theorem is referenced by:  3pm3.2i 818  eqssi 2078  dtruALT 2748  itlso 2863  we0 2944  ordon 2987  ord0 3021  relsn 3254  cnvun 3455  funsn 3543  funi 3545  fnresi 3603  fn0 3605  f0 3656  fconst 3658  f10 3713  f1o0 3716  f1oi 3717  f1osn 3719  fopabsn 3840  fvi 3842  isoid 3895  tfrlem7 3917  tfr1 3924  tz7.44-1 3928  tz7.44-2 3929  frfnom 3951  fo1st 4091  fo2nd 4092  df1st2 4126  df2nd2 4127  oawordeulem 4188  canth2 4484  xpmapenlem5 4500  unfilem2 4549  rankpw 4684  rankuni2 4690  alephiso 4892  alephfplem4 4899  1pi 5011  1pr 5117  axaddopr 5265  axmulopr 5266  axicn 5270  negeu 5355  receu 5701  mulnzcnopr 5702  divval 5704  nnind 5937  0z 6146  elrpi 6283  om2uzuz 6297  om2uzf1o 6301  uzrdgini 6303  uzrdginip1 6305  seq1res 6327  ser1ref 6332  ser1f2 6334  seq1shftid 6356  icoshftf1oi 6409  seq1seqz 6541  seq1seq0 6545  dfseq0 6563  ser0f 6565  sqrlem6 6678  sqrlem23 6695  ref 6759  imf 6760  caure 6927  cauim 6928  ser1absdiflem 6929  serzref 7051  caucvg3a 7164  caucvg3lem 7166  ser1f0 7170  cvgcmp2lem 7180  cvgcmp2clem 7182  cvgcmp3c 7186  isumcmpi 7215  fnsmnt 7226  negfcncf 7269  ivthlem4 7284  ivthlem8 7288  ivthlem9 7289  eff 7313  efaddlem12 7349  eff2 7370  reeff1 7410  eflegeolem2 7414  efcn 7423  reeff1o 7426  reefiso 7428  sinf 7440  cosf 7441  qnnen 7503  ruclem8 7517  ruclem13 7522  ruc 7549  sn0top 7647  indistop 7648  distop 7649  fctopOLD 7650  cctop 7652  retps 7658  ishausi 7785  ismsi 7801  ismeti 7802  0met 7825  metxp 7834  iscms2i 7995  isgrpi 8042  grprn 8056  isgrp2i 8076  isabli 8106  issubgi 8122  ablmul 8131  mulid 8132  ghgrpilem4 8136  cnring 8162  ringsn 8163  nmcnilem 8337  sm1cnilem 8347  ipcl 8365  lnocoi 8418  cnph 8478  cnbn 8528  ubthlem6 8534  minveceu 8583  cnhl 8618  htthlem12 8631  sinco 8667  cosco 8668  pilem2 8672  efif 8721  efifo 8729  efif1 8737  efif1o 8738  eff1i 8744  effoi 8745  eff1oi 8746  pilog 8768  norm3adif 9015  hhip 9044  hhph 9045  hhhl 9073  hlim0 9105  hlimcaui 9106  helch 9116  hsn0elch 9120  hhssnv 9134  hhshsslem2 9138  hhssbn 9151  hhsshl 9152  occl 9181  projlem8 9193  projlemHIL 9218  pjpj0 9255  shscl 9281  shintcl 9293  chintcl 9295  shsumval2 9360  lejdi 9461  osumlem7 9584  nonbool 9596  pjfo 9648  pjf 9649  pjmf1 9661  df0op2 9678  idunop 9902  0cnop 9903  0cnfn 9904  idcnop 9905  idhmop 9906  0hmop 9907  0lnfn 9909  0bdop 9918  lnophs 9926  lnopco 9928  lnopco0 9929  lnopuni 9937  lnophm 9943  nmcopext 9959  nmcoplbt 9960  nmcfnext 9988  nmcfnlbt 9989  nlelsh 9993  nlelch 9994  riesz4 9996  riesz4t 9997  riesz1t 9998  cnlnadjlem6 10005  cnlnadjlem9 10008  cnlnadjeu 10010  cnlnadjeut 10011  nmopadj 10023  bdophs 10029  bdopco 10031  nmopcoadj 10034  pjhmop 10073  pjbdln 10076  hmopidmch 10079  hmopidmpj 10080  mdslj1 10246  ghomsn 10388  cayleylem2 10410  cayleylem3 10411  stcat 10457  dtt2 10618  dmse1 10623  iintlem1 10632  iintlem2 10633  stoi 10639  1alg 10654  1ded 10671  0alg 10689  0ded 10690  0cat 10691  1cat 10692

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