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

Theorem mpbiran 935
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  937  unssdif  3362  unssin  3366  inssun  3367  invdif  3369  pwpwab  3960  exmidexmid  4182  opabm  4265  regexmidlem1  4517  elirr  4525  en2lp  4538  wessep  4562  peano5  4582  relop  4761  ssrnres  5053  funopab  5233  funcnv2  5258  funcnveq  5261  fnres  5314  idref  5736  rnoprab  5936  elixp  6683  djuf1olem  7030  lbfzo0  10137  txdis1cn  13072
  Copyright terms: Public domain W3C validator