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

Theorem mpbir2and 913
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  7214  genpassg  7302  addnqpr  7337  mulnqpr  7353  distrprg  7364  1idpr  7368  ltexpri  7389  recexprlemex  7413  aptipr  7417  cauappcvgprlemladd  7434  ltntri  7858  add20  8204  inelr  8314  recgt0  8576  prodgt0  8578  squeeze0  8630  suprzclex  9117  eluzadd  9322  eluzsub  9323  xrre  9571  xrre3  9573  xleadd1a  9624  elioc2  9687  elico2  9688  elicc2  9689  elfz1eq  9783  fztri3or  9787  fznatpl1  9824  nn0fz0  9867  fzctr  9878  fzo1fzo0n0  9928  fzoaddel  9937  exbtwnz  9996  flid  10025  flqaddz  10038  flqdiv  10062  modqid  10090  frec2uzf1od  10147  iseqf1olemqk  10235  bcval5  10477  abs2difabs  10848  fzomaxdiflem  10852  icodiamlt  10920  dfabsmax  10957  rexico  10961  mul0inf  10980  xrbdtri  11013  sumeq2  11096  sumsnf  11146  fsum00  11199  zsupcllemstep  11565  zssinfcl  11568  gcd0id  11594  gcdneg  11597  nn0seqcvgd  11649  lcmval  11671  lcmneg  11682  qredeq  11704  prmind2  11728  pw2dvdseu  11773  hashdvds  11824  ennnfonelemex  11854  ennnfonelemnn0  11862  tgcl  12160  distop  12181  epttop  12186  neiss  12246  opnneissb  12251  ssnei2  12253  innei  12259  lmconst  12312  cnpnei  12315  cnptopco  12318  cnss1  12322  cnss2  12323  cncnpi  12324  cncnp  12326  cnconst2  12329  cnrest  12331  cnptopresti  12334  cnpdis  12338  lmtopcnp  12346  neitx  12364  tx1cn  12365  tx2cn  12366  txcnp  12367  txcnmpt  12369  txdis1cn  12374  psmetsym  12425  psmetres2  12429  isxmetd  12443  xmetsym  12464  xmetpsmet  12465  metrtri  12473  xblss2ps  12500  xblss2  12501  xblcntrps  12509  xblcntr  12510  bdxmet  12597  bdmet  12598  bdmopn  12600  xmetxp  12603  xmetxpbl  12604  rescncf  12664  cncfco  12674  mulcncflem  12686  mulcncf  12687  suplociccreex  12698  ivthinclemlopn  12710  ivthinclemuopn  12712  cnplimcim  12732  cnplimclemr  12734  limccnpcntop  12740  limccnp2cntop  12742  limccoap  12743  dvidlemap  12756  dvcn  12760  dvaddxxbr  12761  dvmulxxbr  12762  dvcoapbr  12767  dvcjbr  12768  dvrecap  12773  refeq  13150
  Copyright terms: Public domain W3C validator