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

Theorem mpbiran 886
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  888  unssdif  3232  unssin  3236  inssun  3237  invdif  3239  exmidexmid  4022  opabm  4098  regexmidlem1  4339  elirr  4347  en2lp  4360  wessep  4383  peano5  4403  relop  4574  ssrnres  4860  funopab  5035  funcnv2  5060  funcnveq  5063  fnres  5116  idref  5518  rnoprab  5713  djuf1olem  6724  lbfzo0  9557
  Copyright terms: Public domain W3C validator