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

Theorem mpbiran 846
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  848  unssdif  3166  unssin  3170  inssun  3171  invdif  3173  0pss  3259  pssv  3261  opabm  4008  regexmidlem1  4218  elirr  4224  en2lp  4232  peano5  4264  relop  4429  ssrnres  4706  funopab  4878  funcnv2  4902  funcnveq  4905  fnres  4958  idref  5339  rnoprab  5529  lbfzo0  8787  peano5set  9374
  Copyright terms: Public domain W3C validator