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  4092  axsiprim  4094  axins2prim  4096  axins3prim  4097  pw111  4171  cnvkexg  4287  ssetkex  4295  sikexg  4297  ins2kexg  4306  ins3kexg  4307  dfaddc2  4382  nnsucelrlem1  4425  ltfinex  4465  eqpwrelk  4479  eqpw1relk  4480  eqtfinrelk  4487  evenfinex  4504  oddfinex  4505  evenodddisjlem1  4516  nnadjoinlem1  4520  srelk  4525  tfinnnlem1  4534  dfop2lem1  4574  setconslem2  4733  setconslem3  4734  setconslem7  4738  dfswap2  4742  isocnv2  5493  brimage  5794  releqel  5808  releqmpt2  5810  extex  5916  qsexg  5983  ovcelem1  6172  tcfnex  6245