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

Theorem mpbiran 884
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  886  unssdif  3223  unssin  3227  inssun  3228  invdif  3230  exmidexmid  4005  opabm  4081  regexmidlem1  4322  elirr  4330  en2lp  4343  wessep  4366  peano5  4386  relop  4554  ssrnres  4839  funopab  5014  funcnv2  5039  funcnveq  5042  fnres  5095  idref  5497  rnoprab  5688  djuf1olem  6689  lbfzo0  9520
  Copyright terms: Public domain W3C validator