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

Theorem imbi12i 238
 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 225 . 2 ((𝜑𝜒) ↔ (𝜑𝜃))
3 imbi12i.1 . . 3 (𝜑𝜓)
43imbi1i 237 . 2 ((𝜑𝜃) ↔ (𝜓𝜃))
52, 4bitri 183 1 ((𝜑𝜒) ↔ (𝜓𝜃))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 104 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  stdcn  832  nfbii  1449  sbi2v  1864  sbim  1926  sb8mo  2013  cbvmo  2039  necon4ddc  2380  raleqbii  2447  rmo5  2646  cbvrmo  2653  ss2ab  3165  snsssn  3688  trint  4041  ssextss  4142  ordsoexmid  4477  zfregfr  4488  tfi  4496  peano2  4509  peano5  4512  relop  4689  dmcosseq  4810  cotr  4920  issref  4921  cnvsym  4922  intasym  4923  intirr  4925  codir  4927  qfto  4928  cnvpom  5081  cnvsom  5082  funcnvuni  5192  poxp  6129  infmoti  6915  dfinfre  8726  bezoutlembi  11704  algcvgblem  11741  isprm2  11809  ntreq0  12315  ss1oel2o  13294
 Copyright terms: Public domain W3C validator