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  429  bi2bian9  528  cleqh  2115  abbi  2129  cleqf  2179  vtoclb  2584  vtoclbg  2587  ceqsexg  2645  elabgf  2658  reu6  2703  ru  2736  sbcbig  2782  sbcne12g  2841  sbcnestgf  2870  preq12bg  3514  nalset  3857  opthg  3945  opelopabsb  3967  opeliunxp2  4399  resieq  4545  elimasng  4616  cbviota  4795  iota2df  4814  fnbrfvb  5135  fvelimab  5150  fmptco  5251  fsng  5257  fressnfv  5271  funfvima3  5313  isorel  5369  isocnv  5372  isocnv2  5373  isotr  5377  ovg  5558  caovcang  5581  caovordg  5587  caovord3d  5590  caovord  5591  dftpos4  5796  ecopovsym  6109  ecopovsymg  6112  ltanqg  6253  ltmnqg  6254  elinp  6322  prnmaxl  6336  prnminu  6337  ltasrg  6511  axpre-ltadd  6573  bj-nalset  7257  bj-d0clsepcl  7287  bj-nn0sucALT  7335
  Copyright terms: Public domain W3C validator