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

Theorem mpbiran2 908
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 298 . 2  |-  ( ps  <->  ( ps  /\  ch )
)
41, 3bitr4i 186 1  |-  ( ph  <->  ps )
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:  reueq  2854  ss0b  3370  eusv1  4341  eusv2nf  4345  eusv2  4346  opthprc  4558  opelres  4792  f1cnvcnv  5307  fores  5322  f1orn  5343  funfvdm  5450  dfoprab2  5784  tpostpos  6127  opelreal  7599  elreal2  7602  eqresr  7608  axprecex  7652  zeoxor  11462  isprm2  11694  toptopon  12080  bdeq0  12876  subctctexmid  13007
  Copyright terms: Public domain W3C validator