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

Theorem impbida 528
Description: Deduce an equivalence from two implications. (Contributed by NM, 17-Feb-2007.)
Hypotheses
Ref Expression
impbida.1 ((φ ψ) → χ)
impbida.2 ((φ χ) → ψ)
Assertion
Ref Expression
impbida (φ → (ψχ))

Proof of Theorem impbida
StepHypRef Expression
1 impbida.1 . . 3 ((φ ψ) → χ)
21ex 108 . 2 (φ → (ψχ))
3 impbida.2 . . 3 ((φ χ) → ψ)
43ex 108 . 2 (φ → (χψ))
52, 4impbid 120 1 (φ → (ψχ))
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97  wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  eqrdav  2036  funfvbrb  5223  f1ocnv2d  5646  1stconst  5784  2ndconst  5785  cnvf1o  5788  ersymb  6056  swoer  6070  erth  6086  enen1  6247  enen2  6248  domen1  6249  domen2  6250  fzsplit2  8664  fseq1p1m1  8706  elfz2nn0  8723  zesq  9000  rereb  9071
  Copyright terms: Public domain W3C validator