Theorem bibi2d 470

Description: Deduction adding a biconditional to the left in an equivalence.

Hypothesis

Ref	Expression
bid.1	|- (ph -> (ps <-> ch))

Assertion

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

Proof of Theorem bibi2d

Step	Hyp	Ref	Expression
1		bid.1	. . . . 5 |- (ph -> (ps <-> ch))
2	1	imbi2d 464	. . . 4 |- (ph -> ((th -> ps) <-> (th -> ch)))
3	2	anbi1d 469	. . 3 |- (ph -> (((th -> ps) /\ (ps -> th)) <-> ((th -> ch) /\ (ps -> th))))
4	1	imbi1d 465	. . . 4 |- (ph -> ((ps -> th) <-> (ch -> th)))
5	4	anbi2d 468	. . 3 |- (ph -> (((th -> ch) /\ (ps -> th)) <-> ((th -> ch) /\ (ch -> th))))
6	3, 5	bitrd 406	. 2 |- (ph -> (((th -> ps) /\ (ps -> th)) <-> ((th -> ch) /\ (ch -> th))))
7		bi 396	. 2 |- ((th <-> ps) <-> ((th -> ps) /\ (ps -> th)))
8		bi 396	. 2 |- ((th <-> ch) <-> ((th -> ch) /\ (ch -> th)))
9	6, 7, 8	3bitr4g 428	1 |- (ph -> ((th <-> ps) <-> (th <-> ch)))

Syntax hints:   -> wi 2   <-> wb 127   /\ wa 196

This theorem is referenced by:  bibi1d 471  bibi12d 477  biantr 556  euf 1011  axac 1085  ceqex 1410  sbc2or 1454  axrep 1473  axrep2 1474  zfrepclf 1477  copsexg 1902  isoeq1 2925  isoeq3 2927  caoprord 3070  aceq0 3553  aceq5 3563  zfcndrep 3760  zfcndac 3765  ltapq 3870  ltmpq 3871  ltasr 4003  axltadd 4085  ltadd1t 4348  leadd1t 4350  ltmul1 4394  ltdiv 4399  ltdivt 4404

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org