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

Theorem imbi12i 239
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 226 . 2 ((𝜑𝜒) ↔ (𝜑𝜃))
3 imbi12i.1 . . 3 (𝜑𝜓)
43imbi1i 238 . 2 ((𝜑𝜃) ↔ (𝜓𝜃))
52, 4bitri 184 1 ((𝜑𝜒) ↔ (𝜓𝜃))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  stdcn  847  nfbii  1473  sbi2v  1892  sbim  1953  sb8mo  2040  cbvmo  2066  necon4ddc  2419  raleqbii  2489  rmo5  2692  cbvrmo  2702  ss2ab  3223  snsssn  3759  trint  4113  ssextss  4217  ordsoexmid  4558  zfregfr  4570  tfi  4578  peano2  4591  peano5  4594  relop  4773  dmcosseq  4894  cotr  5006  issref  5007  cnvsym  5008  intasym  5009  intirr  5011  codir  5013  qfto  5014  cnvpom  5167  cnvsom  5168  funcnvuni  5281  poxp  6227  infmoti  7021  dfinfre  8899  bezoutlembi  11986  algcvgblem  12029  isprm2  12097  ntreq0  13296  ss1oel2o  14396
  Copyright terms: Public domain W3C validator