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

Theorem mpbiran 907
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 299 . 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  909  unssdif  3279  unssin  3283  inssun  3284  invdif  3286  pwpwab  3868  exmidexmid  4088  opabm  4170  regexmidlem1  4416  elirr  4424  en2lp  4437  wessep  4460  peano5  4480  relop  4657  ssrnres  4949  funopab  5126  funcnv2  5151  funcnveq  5154  fnres  5207  idref  5624  rnoprab  5820  elixp  6565  djuf1olem  6904  lbfzo0  9898  txdis1cn  12342
  Copyright terms: Public domain W3C validator