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

Theorem bibi12i 306
 Description: The equivalence of two equivalences. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
bibi.a (φψ)
bibi12.2 (χθ)
Assertion
Ref Expression
bibi12i ((φχ) ↔ (ψθ))

Proof of Theorem bibi12i
StepHypRef Expression
1 bibi12.2 . . 3 (χθ)
21bibi2i 304 . 2 ((φχ) ↔ (φθ))
3 bibi.a . . 3 (φψ)
43bibi1i 305 . 2 ((φθ) ↔ (ψθ))
52, 4bitri 240 1 ((φχ) ↔ (ψθ))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 176 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8 This theorem depends on definitions:  df-bi 177 This theorem is referenced by:  pm5.32  617  orbidi  898  pm5.7  900  xorbi12i  1314  axcnvprim  4091  axsiprim  4093  axins2prim  4095  axins3prim  4096  pw111  4170  cnvkexg  4286  ssetkex  4294  sikexg  4296  ins2kexg  4305  ins3kexg  4306  dfaddc2  4381  nnsucelrlem1  4424  ltfinex  4464  eqpwrelk  4478  eqpw1relk  4479  eqtfinrelk  4486  evenfinex  4503  oddfinex  4504  evenodddisjlem1  4515  nnadjoinlem1  4519  srelk  4524  tfinnnlem1  4533  dfop2lem1  4573  setconslem2  4732  setconslem3  4733  setconslem7  4737  dfswap2  4741  isocnv2  5492  brimage  5793  releqel  5807  releqmpt2  5809  extex  5915  qsexg  5982  ovcelem1  6171  tcfnex  6244
 Copyright terms: Public domain W3C validator