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

Theorem mpbir2and 851
 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 290 . 2 (𝜑 → (𝜒𝜃))
4 mpbir2and.3 . 2 (𝜑 → (𝜓 ↔ (𝜒𝜃)))
53, 4mpbird 156 1 (𝜑𝜓)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101 This theorem depends on definitions:  df-bi 110 This theorem is referenced by:  nqnq0pi  6536  genpassg  6624  addnqpr  6659  mulnqpr  6675  distrprg  6686  1idpr  6690  ltexpri  6711  recexprlemex  6735  aptipr  6739  cauappcvgprlemladd  6756  add20  7469  inelr  7575  recgt0  7816  prodgt0  7818  squeeze0  7870  eluzadd  8501  eluzsub  8502  xrre  8733  xrre3  8735  elioc2  8805  elico2  8806  elicc2  8807  elfz1eq  8899  fztri3or  8903  fznatpl1  8938  nn0fz0  8978  fzctr  8991  fzo1fzo0n0  9039  fzoaddel  9048  qbtwnz  9106  flid  9126  flqaddz  9139  flqdiv  9163  frec2uzf1od  9192  expival  9257  abs2difabs  9704  fzomaxdiflem  9708  icodiamlt  9776  nn0seqcvgd  9880
 Copyright terms: Public domain W3C validator