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

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

Proof of Theorem mpbiran2
StepHypRef Expression
1 mpbiran2.2 . 2  |-  ( ph  <->  ( ps  /\  ch )
)
2 mpbiran2.1 . . 3  |-  ch
32biantru 296 . 2  |-  ( ps  <->  ( ps  /\  ch )
)
41, 3bitr4i 185 1  |-  ( ph  <->  ps )
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:  reueq  2790  ss0b  3284  eusv1  4204  eusv2nf  4208  eusv2  4209  opthprc  4411  opelres  4639  f1cnvcnv  5125  fores  5140  f1orn  5161  funfvdm  5262  dfoprab2  5577  tpostpos  5907  opelreal  7047  elreal2  7050  eqresr  7055  axprecex  7097  zeoxor  10402  isprm2  10632  bdeq0  10801
  Copyright terms: Public domain W3C validator