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

Theorem mpbiran 925
 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  927  unssdif  3312  unssin  3316  inssun  3317  invdif  3319  pwpwab  3904  exmidexmid  4124  opabm  4206  regexmidlem1  4452  elirr  4460  en2lp  4473  wessep  4496  peano5  4516  relop  4693  ssrnres  4985  funopab  5162  funcnv2  5187  funcnveq  5190  fnres  5243  idref  5662  rnoprab  5858  elixp  6603  djuf1olem  6942  lbfzo0  9985  txdis1cn  12477
 Copyright terms: Public domain W3C validator