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

Theorem mpbiran2 887
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  2812  ss0b  3319  eusv1  4265  eusv2nf  4269  eusv2  4270  opthprc  4477  opelres  4706  f1cnvcnv  5211  fores  5226  f1orn  5247  funfvdm  5351  dfoprab2  5678  tpostpos  6011  opelreal  7344  elreal2  7347  eqresr  7352  axprecex  7394  zeoxor  10962  isprm2  11192  bdeq0  11415
  Copyright terms: Public domain W3C validator