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

Theorem imbi12i 237
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 224 . 2 ((𝜑𝜒) ↔ (𝜑𝜃))
3 imbi12i.1 . . 3 (𝜑𝜓)
43imbi1i 236 . 2 ((𝜑𝜃) ↔ (𝜓𝜃))
52, 4bitri 182 1 ((𝜑𝜒) ↔ (𝜓𝜃))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  nfbii  1407  sbi2v  1820  sbim  1875  sb8mo  1962  cbvmo  1988  necon4ddc  2327  raleqbii  2390  rmo5  2582  cbvrmo  2589  ss2ab  3089  snsssn  3605  trint  3951  ssextss  4047  ordsoexmid  4378  zfregfr  4389  tfi  4397  peano2  4410  peano5  4413  relop  4586  dmcosseq  4704  cotr  4813  issref  4814  cnvsym  4815  intasym  4816  intirr  4818  codir  4820  qfto  4821  cnvpom  4973  cnvsom  4974  funcnvuni  5083  poxp  5997  infmoti  6721  dfinfre  8415  bezoutlembi  11268  algcvgblem  11305  isprm2  11373  ss1oel2o  11843
  Copyright terms: Public domain W3C validator