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

Theorem mpbiran2 926
Description: Detach truth from conjunction in biconditional. (Contributed by NM, 22-Feb-1996.) (Revised by NM, 9-Jan-2015.)
Hypotheses
Ref Expression
mpbiran2.1 𝜒
mpbiran2.2 (𝜑 ↔ (𝜓𝜒))
Assertion
Ref Expression
mpbiran2 (𝜑𝜓)

Proof of Theorem mpbiran2
StepHypRef Expression
1 mpbiran2.2 . 2 (𝜑 ↔ (𝜓𝜒))
2 mpbiran2.1 . . 3 𝜒
32biantru 300 . 2 (𝜓 ↔ (𝜓𝜒))
41, 3bitr4i 186 1 (𝜑𝜓)
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  2886  ss0b  3406  eusv1  4380  eusv2nf  4384  eusv2  4385  opthprc  4597  opelres  4831  f1cnvcnv  5346  fores  5361  f1orn  5384  funfvdm  5491  dfoprab2  5825  tpostpos  6168  opelreal  7658  elreal2  7661  eqresr  7667  axprecex  7711  zeoxor  11600  isprm2  11832  toptopon  12222  bdeq0  13234  subctctexmid  13367
  Copyright terms: Public domain W3C validator