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

Theorem imbi12i 232
 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 219 . 2 ((𝜑𝜒) ↔ (𝜑𝜃))
3 imbi12i.1 . . 3 (𝜑𝜓)
43imbi1i 231 . 2 ((𝜑𝜃) ↔ (𝜓𝜃))
52, 4bitri 177 1 ((𝜑𝜒) ↔ (𝜓𝜃))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 102 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105 This theorem depends on definitions:  df-bi 114 This theorem is referenced by:  nfbii  1378  sbi2v  1788  sbim  1843  sb8mo  1930  cbvmo  1956  necon4ddc  2292  raleqbii  2353  rmo5  2542  cbvrmo  2549  ss2ab  3036  snsssn  3560  trint  3897  ssextss  3984  ordsoexmid  4314  zfregfr  4326  tfi  4333  peano2  4346  peano5  4349  relop  4514  dmcosseq  4631  cotr  4734  issref  4735  cnvsym  4736  intasym  4737  intirr  4739  codir  4741  qfto  4742  cnvpom  4888  cnvsom  4889  funcnvuni  4996  poxp  5881  algcvgblem  10271  peano5setOLD  10452
 Copyright terms: Public domain W3C validator