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

Theorem mpbiran 882
 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 297 . 2 (𝜒 ↔ (𝜓𝜒))
41, 3bitr4i 185 1 (𝜑𝜒)
 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:  mpbir2an  884  unssdif  3215  unssin  3219  inssun  3220  invdif  3222  exmidexmid  3987  opabm  4063  regexmidlem1  4304  elirr  4312  en2lp  4325  wessep  4348  peano5  4367  relop  4534  ssrnres  4813  funopab  4985  funcnv2  5010  funcnveq  5013  fnres  5066  idref  5449  rnoprab  5639  djulf1o  6556  djurf1o  6557  lbfzo0  9337
 Copyright terms: Public domain W3C validator