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

Theorem mpbiran 882
Description: Detach truth from conjunction in biconditional. (Contributed by NM, 27-Feb-1996.) (Revised by NM, 9-Jan-2015.)
Hypotheses
Ref Expression
mpbiran.1  |-  ps
mpbiran.2  |-  ( ph  <->  ( ps  /\  ch )
)
Assertion
Ref Expression
mpbiran  |-  ( ph  <->  ch )

Proof of Theorem mpbiran
StepHypRef Expression
1 mpbiran.2 . 2  |-  ( ph  <->  ( ps  /\  ch )
)
2 mpbiran.1 . . 3  |-  ps
32biantrur 297 . 2  |-  ( ch  <->  ( ps  /\  ch )
)
41, 3bitr4i 185 1  |-  ( ph  <->  ch )
Colors of variables: wff set class
Syntax hints:    /\ 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:  mpbir2an  884  unssdif  3215  unssin  3219  inssun  3220  invdif  3222  exmidexmid  3987  opabm  4063  regexmidlem1  4304  elirr  4312  en2lp  4325  wessep  4348  peano5  4367  relop  4534  ssrnres  4813  funopab  4985  funcnv2  5010  funcnveq  5013  fnres  5066  idref  5448  rnoprab  5638  djulf1o  6554  djurf1o  6555  lbfzo0  9319
  Copyright terms: Public domain W3C validator