Theorem bibi12i 329

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

Hypotheses

Ref	Expression
bibi2i.1	|- ( ph <-> ps )
bibi12i.2	|- ( ch <-> th )

Assertion

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

Proof of Theorem bibi12i

Step	Hyp	Ref	Expression
1		bibi12i.2	. . 3 |- ( ch <-> th )
2	1	bibi2i 327	. 2 |- ( ( ph <-> ch ) <-> ( ph <-> th ) )
3		bibi2i.1	. . 3 |- ( ph <-> ps )
4	3	bibi1i 328	. 2 |- ( ( ph <-> th ) <-> ( ps <-> th ) )
5	2, 4	bitri 264	1 |- ( ( ph <-> ch ) <-> ( ps <-> th ) )

Syntax hints:   <-> wb 196

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 197

This theorem is referenced by:  pm5.32  668  orbidi  973  pm5.7  975  xorbi12i  1477  abbi  2737  brsymdif  4711  nfnid  4897  asymref  5512  isocnv2  6581  zfcndrep  9436  f1omvdco3  17869  brtxpsd  32001  bj-sbeq  32896  rp-fakeoranass  37859  rp-fakeinunass  37861  relexp0eq  37993