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

Theorem mpbir2and 888
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 300 . 2 (𝜑 → (𝜒𝜃))
4 mpbir2and.3 . 2 (𝜑 → (𝜓 ↔ (𝜒𝜃)))
53, 4mpbird 165 1 (𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  nqnq0pi  6944  genpassg  7032  addnqpr  7067  mulnqpr  7083  distrprg  7094  1idpr  7098  ltexpri  7119  recexprlemex  7143  aptipr  7147  cauappcvgprlemladd  7164  add20  7899  inelr  8005  recgt0  8249  prodgt0  8251  squeeze0  8303  suprzclex  8780  eluzadd  8982  eluzsub  8983  xrre  9217  xrre3  9219  elioc2  9289  elico2  9290  elicc2  9291  elfz1eq  9384  fztri3or  9388  fznatpl1  9423  nn0fz0  9464  fzctr  9475  fzo1fzo0n0  9525  fzoaddel  9534  exbtwnz  9593  flid  9622  flqaddz  9635  flqdiv  9659  modqid  9687  frec2uzf1od  9744  iseqf1olemqk  9847  expival  9877  ibcval5  10089  abs2difabs  10458  fzomaxdiflem  10462  icodiamlt  10530  dfabsmax  10567  rexico  10571  sumeq2  10662  sumsnf  10710  zsupcllemstep  10866  zssinfcl  10869  gcd0id  10895  gcdneg  10898  nn0seqcvgd  10948  lcmval  10970  lcmneg  10981  qredeq  11003  prmind2  11027  pw2dvdseu  11071  hashdvds  11122
  Copyright terms: Public domain W3C validator