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

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

Proof of Theorem mpbiran
StepHypRef Expression
1 mpbiran.2 . 2 (𝜑 ↔ (𝜓𝜒))
2 mpbiran.1 . . 3 𝜓
32biantrur 301 . 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:  mpbir2an  911  unssdif  3281  unssin  3285  inssun  3286  invdif  3288  pwpwab  3870  exmidexmid  4090  opabm  4172  regexmidlem1  4418  elirr  4426  en2lp  4439  wessep  4462  peano5  4482  relop  4659  ssrnres  4951  funopab  5128  funcnv2  5153  funcnveq  5156  fnres  5209  idref  5626  rnoprab  5822  elixp  6567  djuf1olem  6906  lbfzo0  9913  txdis1cn  12358
  Copyright terms: Public domain W3C validator