Theorem bibi2d 620

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 614	. . . 4 |- (ph -> ((th -> ps) <-> (th -> ch)))
3	2	anbi1d 619	. . 3 |- (ph -> (((th -> ps) /\ (ps -> th)) <-> ((th -> ch) /\ (ps -> th))))
4	1	imbi1d 615	. . . 4 |- (ph -> ((ps -> th) <-> (ch -> th)))
5	4	anbi2d 618	. . 3 |- (ph -> (((th -> ch) /\ (ps -> th)) <-> ((th -> ch) /\ (ch -> th))))
6	3, 5	bitrd 530	. 2 |- (ph -> (((th -> ps) /\ (ps -> th)) <-> ((th -> ch) /\ (ch -> th))))
7		dfbi2 516	. 2 |- ((th <-> ps) <-> ((th -> ps) /\ (ps -> th)))
8		dfbi2 516	. 2 |- ((th <-> ch) <-> ((th -> ch) /\ (ch -> th)))
9	6, 7, 8	3bitr4g 557	1 |- (ph -> ((th <-> ps) <-> (th <-> ch)))

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223

This theorem is referenced by:  bibi1d 621  bibi12d 631  biantr 744  euf 1386  ceqex 1889  sbc2or 1961  axrep1 2699  axrep2 2700  axrep3 2701  zfrepclf 2704  axsep2 2709  zfauscl 2710  copsexg 2798  isoeq1 3893  isoeq3 3895  caoprord 4062  aceq0 4740  aceq5 4750  axac 4755  zfcndrep 4978  zfcndac 4983  ltapq 5088  ltmpq 5089  ltasr 5221  pre-axltadd 5301  ltadd1t 5635  leadd1t 5637  ltmul1 5824  ltdiv1 5826  ltmul1t 5832  ltdiv1t 5851  ltdiv1tOLD 5852  clm4at 7090  eigret 9756  isded 10640  dedi 10641

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

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain