ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  imbi12i 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  1362  sbi2v  1772  sbim  1827  sb8mo  1914  cbvmo  1940  necon4ddc  2277  raleqbii  2336  rmo5  2525  cbvrmo  2532  ss2ab  3008  snsssn  3532  trint  3869  ssextss  3956  ordsoexmid  4286  zfregfr  4298  tfi  4305  peano2  4318  peano5  4321  relop  4486  dmcosseq  4603  cotr  4706  issref  4707  cnvsym  4708  intasym  4709  intirr  4711  codir  4713  qfto  4714  cnvpom  4860  cnvsom  4861  funcnvuni  4968  poxp  5853  algcvgblem  9888  peano5setOLD  10065
  Copyright terms: Public domain W3C validator