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

Theorem imbi12i 228
Description: Join two logical equivalences to form equivalence of implications. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
imbi12i.1 (φψ)
imbi12i.2 (χθ)
Assertion
Ref Expression
imbi12i ((φχ) ↔ (ψθ))

Proof of Theorem imbi12i
StepHypRef Expression
1 imbi12i.2 . . 3 (χθ)
21imbi2i 215 . 2 ((φχ) ↔ (φθ))
3 imbi12i.1 . . 3 (φψ)
43imbi1i 227 . 2 ((φθ) ↔ (ψθ))
52, 4bitri 173 1 ((φχ) ↔ (ψθ))
Colors of variables: wff set class
Syntax hints:  wi 4  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:  nfbii  1338  sbi2v  1750  sbim  1805  sb8mo  1892  cbvmo  1918  necon4ddc  2251  raleqbii  2310  rmo5  2499  cbvrmo  2506  ss2ab  2981  snsssn  3502  trint  3839  ssextss  3926  ordsoexmid  4220  tfi  4228  peano2  4241  peano5  4244  relop  4409  dmcosseq  4526  cotr  4629  issref  4630  cnvsym  4631  intasym  4632  intirr  4634  codir  4636  qfto  4637  cnvpom  4783  cnvsom  4784  funcnvuni  4890  poxp  5771  peano5set  7301
  Copyright terms: Public domain W3C validator