NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  bibi12d GIF version

Theorem bibi12d 312
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 310 . 2 (φ → ((ψθ) ↔ (χθ)))
3 imbi12d.2 . . 3 (φ → (θτ))
43bibi2d 309 . 2 (φ → ((χθ) ↔ (χτ)))
52, 4bitrd 244 1 (φ → ((ψθ) ↔ (χτ)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 176
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 177
This theorem is referenced by:  bi2bian9  845  xorbi12d  1315  cleqh  2450  abbi  2463  cleqf  2513  vtoclb  2912  vtoclbg  2915  ceqsexg  2970  elabgf  2983  reu6  3025  ru  3045  sbcbig  3092  sbcnestgf  3183  unineq  3505  preq12bg  4128  eqpw1  4162  pw111  4170  eqrelk  4212  opkelimagekg  4271  sikexlem  4295  insklem  4304  eqpw1uni  4330  cbviota  4344  iota2df  4365  opelopabsb  4697  br1stg  4730  opeliunxp2  4822  fvelimab  5370  eqfnfv  5392  fsng  5433  fressnfv  5439  isorel  5489  isocnv  5491  isotr  5495  caovord  5629  trtxp  5781  oqelins4  5794  txpcofun  5803  qrpprod  5836  fnfullfunlem1  5856  clos1basesucg  5884  extd  5923  xpassen  6057  enpw1  6062  dflec3  6221  lenc  6223  tc11  6228
  Copyright terms: Public domain W3C validator