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

Theorem mpbiran 847
 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 287 . 2 (𝜒 ↔ (𝜓𝜒))
41, 3bitr4i 176 1 (𝜑𝜒)
 Colors of variables: wff set class Syntax hints:   ∧ wa 97   ↔ wb 98 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101 This theorem depends on definitions:  df-bi 110 This theorem is referenced by:  mpbir2an  849  unssdif  3172  unssin  3176  inssun  3177  invdif  3179  0pss  3265  pssv  3267  opabm  4017  regexmidlem1  4258  elirr  4266  en2lp  4278  wessep  4302  peano5  4321  relop  4486  ssrnres  4763  funopab  4935  funcnv2  4959  funcnveq  4962  fnres  5015  idref  5396  rnoprab  5587  lbfzo0  9037  peano5setOLD  10065
 Copyright terms: Public domain W3C validator