Theorem mpbir2an 732

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

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

This theorem is referenced by:  3pm3.2i 820  eqssi 2082  dtruALT 2755  itlso 2870  we0 2951  ordon 2994  ord0 3028  relsn 3261  cnvun 3462  funsn 3550  funi 3552  fnresi 3610  fn0 3612  f0 3663  fconst 3665  f10 3720  f1o0 3723  f1oi 3724  f1osn 3726  fopabsn 3847  fvi 3849  isoid 3902  tfrlem7 3924  tfr1 3931  tz7.44-1 3935  tz7.44-2 3936  frfnom 3958  fo1st 4098  fo2nd 4099  df1st2 4133  df2nd2 4134  oawordeulem 4195  canth2 4491  xpmapenlem5 4507  unfilem2 4563  rankpw 4701  rankuni2 4707  alephiso 4910  alephfplem4 4917  1pi 5030  1pr 5136  axaddopr 5284  axmulopr 5285  axicn 5289  negeu 5374  receu 5720  mulnzcnopr 5721  divval 5723  nnind 5946  0z 6155  elrpi 6291  om2uzuz 6305  om2uzf1o 6309  uzrdgini 6311  uzrdginip1 6313  seq1res 6335  ser1ref 6340  ser1f2 6342  seq1shftid 6364  icoshftf1oi 6417  seq1seqz 6549  seq1seq0 6553  dfseq0 6571  ser0f 6573  sqrlem6 6686  sqrlem23 6703  ref 6767  imf 6768  caure 6934  cauim 6935  ser1absdiflem 6936  serzref 7058  caucvg3a 7171  caucvg3lem 7173  ser1f0 7177  cvgcmp2lem 7187  cvgcmp2clem 7189  cvgcmp3c 7193  isumcmpi 7222  fnsmnt 7233  negfcncf 7276  ivthlem4 7291  ivthlem8 7295  ivthlem9 7296  eff 7320  efaddlem12 7356  eff2 7377  reeff1 7417  eflegeolem2 7421  efcn 7430  reeff1o 7433  reefiso 7435  sinf 7447  cosf 7448  qnnen 7511  ruclem8 7525  ruclem13 7530  ruc 7557  sn0top 7651  indistop 7652  distop 7653  fctopOLD 7654  cctop 7656  retps 7662  ishausi 7789  ismsi 7805  ismeti 7806  0met 7829  metxp 7838  iscms2i 7999  isgrpi 8046  grprn 8060  isgrp2i 8079  isabli 8109  issubgi 8125  ablmul 8134  mulid 8135  ghgrpilem4 8139  cnring 8165  ringsn 8166  nmcnilem 8340  sm1cnilem 8350  ipcl 8368  lnocoi 8421  cnph 8481  cnbn 8531  ubthlem6 8537  minveceu 8586  cnhl 8621  htthlem12 8634  sinco 8669  cosco 8670  pilem2 8674  efif 8723  efifo 8731  efif1 8739  efif1o 8740  eff1i 8746  effoi 8747  eff1oi 8748  pilog 8770  norm3adif 9017  hhip 9046  hhph 9047  hhhl 9075  hlim0 9107  hlimcaui 9108  helch 9118  hsn0elch 9122  hhssnv 9136  hhshsslem2 9140  hhssbn 9153  hhsshl 9154  occl 9183  projlem8 9195  projlemHIL 9220  pjpj0 9257  shscl 9283  shintcl 9295  chintcl 9297  shsumval2 9362  lejdi 9463  osumlem7 9586  nonbool 9598  pjfo 9650  pjf 9651  pjmf1 9663  df0op2 9680  idunop 9904  0cnop 9905  0cnfn 9906  idcnop 9907  idhmop 9908  0hmop 9909  0lnfn 9911  0bdop 9920  lnophs 9928  lnopco 9930  lnopco0 9931  lnopuni 9939  lnophm 9945  nmcopext 9961  nmcoplbt 9962  nmcfnext 9990  nmcfnlbt 9991  nlelsh 9995  nlelch 9996  riesz4 9998  riesz4t 9999  riesz1t 10000  cnlnadjlem6 10007  cnlnadjlem9 10010  cnlnadjeu 10012  cnlnadjeut 10013  nmopadj 10025  bdophs 10031  bdopco 10033  nmopcoadj 10036  pjhmop 10075  pjbdln 10078  hmopidmch 10081  hmopidmpj 10082  mdslj1 10249  ghomsn 10391  cayleylem2 10413  cayleylem3 10414  stcat 10455  vxveqv 10475  dtt2 10597  stoi 10618  1alg 10633  1ded 10650  0alg 10668  0ded 10669  0cat 10670  1cat 10671

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