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

Theorem mpbir2and 911
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 (𝜑𝜒)
mpbir2and.2 (𝜑𝜃)
mpbir2and.3 (𝜑 → (𝜓 ↔ (𝜒𝜃)))
Assertion
Ref Expression
mpbir2and (𝜑𝜓)

Proof of Theorem mpbir2and
StepHypRef Expression
1 mpbir2and.1 . . 3 (𝜑𝜒)
2 mpbir2and.2 . . 3 (𝜑𝜃)
31, 2jca 302 . 2 (𝜑 → (𝜒𝜃))
4 mpbir2and.3 . 2 (𝜑 → (𝜓 ↔ (𝜒𝜃)))
53, 4mpbird 166 1 (𝜑𝜓)
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  7210  genpassg  7298  addnqpr  7333  mulnqpr  7349  distrprg  7360  1idpr  7364  ltexpri  7385  recexprlemex  7409  aptipr  7413  cauappcvgprlemladd  7430  ltntri  7854  add20  8200  inelr  8309  recgt0  8565  prodgt0  8567  squeeze0  8619  suprzclex  9100  eluzadd  9303  eluzsub  9304  xrre  9543  xrre3  9545  xleadd1a  9596  elioc2  9659  elico2  9660  elicc2  9661  elfz1eq  9755  fztri3or  9759  fznatpl1  9796  nn0fz0  9839  fzctr  9850  fzo1fzo0n0  9900  fzoaddel  9909  exbtwnz  9968  flid  9997  flqaddz  10010  flqdiv  10034  modqid  10062  frec2uzf1od  10119  iseqf1olemqk  10207  bcval5  10449  abs2difabs  10820  fzomaxdiflem  10824  icodiamlt  10892  dfabsmax  10929  rexico  10933  mul0inf  10952  xrbdtri  10985  sumeq2  11068  sumsnf  11118  fsum00  11171  zsupcllemstep  11534  zssinfcl  11537  gcd0id  11563  gcdneg  11566  nn0seqcvgd  11618  lcmval  11640  lcmneg  11651  qredeq  11673  prmind2  11697  pw2dvdseu  11741  hashdvds  11792  ennnfonelemex  11822  ennnfonelemnn0  11830  tgcl  12128  distop  12149  epttop  12154  neiss  12214  opnneissb  12219  ssnei2  12221  innei  12227  lmconst  12280  cnpnei  12283  cnptopco  12286  cnss1  12290  cnss2  12291  cncnpi  12292  cncnp  12294  cnconst2  12297  cnrest  12299  cnptopresti  12302  cnpdis  12306  lmtopcnp  12314  neitx  12332  tx1cn  12333  tx2cn  12334  txcnp  12335  txcnmpt  12337  txdis1cn  12342  psmetsym  12393  psmetres2  12397  isxmetd  12411  xmetsym  12432  xmetpsmet  12433  metrtri  12441  xblss2ps  12468  xblss2  12469  xblcntrps  12477  xblcntr  12478  bdxmet  12565  bdmet  12566  bdmopn  12568  xmetxp  12571  xmetxpbl  12572  rescncf  12632  cncfco  12642  mulcncflem  12654  mulcncf  12655  suplociccreex  12666  cnplimcim  12688  cnplimclemr  12690  limccnpcntop  12696  limccnp2cntop  12698  limccoap  12699  dvidlemap  12712  dvcn  12716  dvaddxxbr  12717  dvmulxxbr  12718  dvcoapbr  12723  dvcjbr  12724  dvrecap  12729  refeq  13034
  Copyright terms: Public domain W3C validator