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

Theorem mpbiran 833
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  835  unssdif  3145  unssin  3149  inssun  3150  invdif  3152  0pss  3238  pssv  3240  opabm  3987  regexmidlem1  4198  elirr  4204  en2lp  4212  peano5  4244  relop  4409  ssrnres  4686  funopab  4857  funcnv2  4881  funcnveq  4884  fnres  4937  idref  5317  rnoprab  5506  peano5set  7301
  Copyright terms: Public domain W3C validator