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

Theorem bibi12d 224
Description: Deduction joining two equivalences to form equivalence of biconditionals. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
imbi12d.1 (φ → (ψχ))
imbi12d.2 (φ → (θτ))
Assertion
Ref Expression
bibi12d (φ → ((ψθ) ↔ (χτ)))

Proof of Theorem bibi12d
StepHypRef Expression
1 imbi12d.1 . . 3 (φ → (ψχ))
21bibi1d 222 . 2 (φ → ((ψθ) ↔ (χθ)))
3 imbi12d.2 . . 3 (φ → (θτ))
43bibi2d 221 . 2 (φ → ((χθ) ↔ (χτ)))
52, 4bitrd 177 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:  pm5.32  426  bi2bian9  540  cleqh  2134  abbi  2148  cleqf  2198  vtoclb  2605  vtoclbg  2608  ceqsexg  2666  elabgf  2679  reu6  2724  ru  2757  sbcbig  2803  sbcne12g  2862  sbcnestgf  2891  preq12bg  3535  nalset  3878  opthg  3966  opelopabsb  3988  opeliunxp2  4419  resieq  4565  elimasng  4636  cbviota  4815  iota2df  4834  fnbrfvb  5157  fvelimab  5172  fmptco  5273  fsng  5279  fressnfv  5293  funfvima3  5335  isorel  5391  isocnv  5394  isocnv2  5395  isotr  5399  ovg  5581  caovcang  5604  caovordg  5610  caovord3d  5613  caovord  5614  dftpos4  5819  ecopovsym  6138  ecopovsymg  6141  ltanqg  6384  ltmnqg  6385  elinp  6456  prnmaxl  6470  prnminu  6471  ltasrg  6678  axpre-ltadd  6750  zextle  8087  zextlt  8088  bj-nalset  9326  bj-d0clsepcl  9360  bj-nn0sucALT  9408
  Copyright terms: Public domain W3C validator