Theorem bibi12i 306

Description: The equivalence of two equivalences. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
bibi.a	|- (ph <-> ps)
bibi12.2	|- (ch <-> th)

Assertion

Ref	Expression
bibi12i	|- ((ph <-> ch) <-> (ps <-> th))

Proof of Theorem bibi12i

Step	Hyp	Ref	Expression
1		bibi12.2	. . 3 |- (ch <-> th)
2	1	bibi2i 304	. 2 |- ((ph <-> ch) <-> (ph <-> th))
3		bibi.a	. . 3 |- (ph <-> ps)
4	3	bibi1i 305	. 2 |- ((ph <-> th) <-> (ps <-> th))
5	2, 4	bitri 240	1 |- ((ph <-> ch) <-> (ps <-> th))

Syntax hints:   <-> 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:  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