ILE Home 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  6534  genpassg  6622  addnqpr  6657  mulnqpr  6673  distrprg  6684  1idpr  6688  ltexpri  6709  recexprlemex  6733  aptipr  6737  cauappcvgprlemladd  6754  add20  7467  inelr  7573  recgt0  7814  prodgt0  7816  squeeze0  7868  eluzadd  8499  eluzsub  8500  xrre  8731  xrre3  8733  elioc2  8803  elico2  8804  elicc2  8805  elfz1eq  8897  fztri3or  8901  fznatpl1  8936  nn0fz0  8976  fzctr  8989  fzo1fzo0n0  9037  fzoaddel  9046  qbtwnz  9104  flid  9124  flqaddz  9137  frec2uzf1od  9166  expival  9231  abs2difabs  9678  fzomaxdiflem  9682  icodiamlt  9750  nn0seqcvgd  9853
  Copyright terms: Public domain W3C validator