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

Theorem mpbiran 925
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 301 . 2  |-  ( ch  <->  ( ps  /\  ch )
)
41, 3bitr4i 186 1  |-  ( ph  <->  ch )
Colors of variables: wff set class
Syntax hints:    /\ 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:  mpbir2an  927  unssdif  3342  unssin  3346  inssun  3347  invdif  3349  pwpwab  3936  exmidexmid  4157  opabm  4240  regexmidlem1  4492  elirr  4500  en2lp  4513  wessep  4537  peano5  4557  relop  4736  ssrnres  5028  funopab  5205  funcnv2  5230  funcnveq  5233  fnres  5286  idref  5707  rnoprab  5904  elixp  6650  djuf1olem  6997  lbfzo0  10080  txdis1cn  12678
  Copyright terms: Public domain W3C validator