ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mpbir2and Unicode version

Theorem mpbir2and 928
Description: Detach a conjunction of truths in a biconditional. (Contributed by NM, 6-Nov-2011.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
Hypotheses
Ref Expression
mpbir2and.1  |-  ( ph  ->  ch )
mpbir2and.2  |-  ( ph  ->  th )
mpbir2and.3  |-  ( ph  ->  ( ps  <->  ( ch  /\ 
th ) ) )
Assertion
Ref Expression
mpbir2and  |-  ( ph  ->  ps )

Proof of Theorem mpbir2and
StepHypRef Expression
1 mpbir2and.1 . . 3  |-  ( ph  ->  ch )
2 mpbir2and.2 . . 3  |-  ( ph  ->  th )
31, 2jca 304 . 2  |-  ( ph  ->  ( ch  /\  th ) )
4 mpbir2and.3 . 2  |-  ( ph  ->  ( ps  <->  ( ch  /\ 
th ) ) )
53, 4mpbird 166 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    <-> wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  nqnq0pi  7260  genpassg  7348  addnqpr  7383  mulnqpr  7399  distrprg  7410  1idpr  7414  ltexpri  7435  recexprlemex  7459  aptipr  7463  cauappcvgprlemladd  7480  ltntri  7904  add20  8250  inelr  8360  recgt0  8622  prodgt0  8624  squeeze0  8676  suprzclex  9163  eluzadd  9368  eluzsub  9369  xrre  9617  xrre3  9619  xleadd1a  9670  elioc2  9733  elico2  9734  elicc2  9735  elfz1eq  9829  fztri3or  9833  fznatpl1  9870  nn0fz0  9913  fzctr  9924  fzo1fzo0n0  9974  fzoaddel  9983  exbtwnz  10042  flid  10071  flqaddz  10084  flqdiv  10108  modqid  10136  frec2uzf1od  10193  iseqf1olemqk  10281  bcval5  10523  abs2difabs  10894  fzomaxdiflem  10898  icodiamlt  10966  dfabsmax  11003  rexico  11007  mul0inf  11026  xrbdtri  11059  sumeq2  11142  sumsnf  11192  fsum00  11245  prodeq2  11340  zsupcllemstep  11651  zssinfcl  11654  gcd0id  11680  gcdneg  11683  nn0seqcvgd  11735  lcmval  11757  lcmneg  11768  qredeq  11790  prmind2  11814  pw2dvdseu  11859  hashdvds  11910  ennnfonelemex  11940  ennnfonelemnn0  11948  tgcl  12249  distop  12270  epttop  12275  neiss  12335  opnneissb  12340  ssnei2  12342  innei  12348  lmconst  12401  cnpnei  12404  cnptopco  12407  cnss1  12411  cnss2  12412  cncnpi  12413  cncnp  12415  cnconst2  12418  cnrest  12420  cnptopresti  12423  cnpdis  12427  lmtopcnp  12435  neitx  12453  tx1cn  12454  tx2cn  12455  txcnp  12456  txcnmpt  12458  txdis1cn  12463  psmetsym  12514  psmetres2  12518  isxmetd  12532  xmetsym  12553  xmetpsmet  12554  metrtri  12562  xblss2ps  12589  xblss2  12590  xblcntrps  12598  xblcntr  12599  bdxmet  12686  bdmet  12687  bdmopn  12689  xmetxp  12692  xmetxpbl  12693  rescncf  12753  cncfco  12763  mulcncflem  12775  mulcncf  12776  suplociccreex  12787  ivthinclemlopn  12799  ivthinclemuopn  12801  cnplimcim  12821  cnplimclemr  12823  limccnpcntop  12829  limccnp2cntop  12831  limccoap  12832  dvidlemap  12845  dvcn  12849  dvaddxxbr  12850  dvmulxxbr  12851  dvcoapbr  12856  dvcjbr  12857  dvrecap  12862  rpabscxpbnd  13039  refeq  13332  apdifflemf  13348
  Copyright terms: Public domain W3C validator