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

Theorem mpbiran2 847
 Description: Detach truth from conjunction in biconditional. (Contributed by NM, 22-Feb-1996.) (Revised by NM, 9-Jan-2015.)
Hypotheses
Ref Expression
mpbiran2.1 χ
mpbiran2.2 (φ ↔ (ψ χ))
Assertion
Ref Expression
mpbiran2 (φψ)

Proof of Theorem mpbiran2
StepHypRef Expression
1 mpbiran2.2 . 2 (φ ↔ (ψ χ))
2 mpbiran2.1 . . 3 χ
32biantru 286 . 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:  reueq  2732  ss0b  3250  eusv1  4150  eusv2nf  4154  eusv2  4155  opthprc  4334  opelres  4560  f1cnvcnv  5043  fores  5058  f1orn  5079  funfvdm  5179  dfoprab2  5494  tpostpos  5820  opelreal  6726  elreal2  6728  eqresr  6733  axprecex  6764  bdeq0  9322
 Copyright terms: Public domain W3C validator