Theorem bibi2d 617

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 611	. . . 4 |- (ph -> ((th -> ps) <-> (th -> ch)))
3	2	anbi1d 616	. . 3 |- (ph -> (((th -> ps) /\ (ps -> th)) <-> ((th -> ch) /\ (ps -> th))))
4	1	imbi1d 612	. . . 4 |- (ph -> ((ps -> th) <-> (ch -> th)))
5	4	anbi2d 615	. . 3 |- (ph -> (((th -> ch) /\ (ps -> th)) <-> ((th -> ch) /\ (ch -> th))))
6	3, 5	bitrd 527	. 2 |- (ph -> (((th -> ps) /\ (ps -> th)) <-> ((th -> ch) /\ (ch -> th))))
7		bi 514	. 2 |- ((th <-> ps) <-> ((th -> ps) /\ (ps -> th)))
8		bi 514	. 2 |- ((th <-> ch) <-> ((th -> ch) /\ (ch -> th)))
9	6, 7, 8	3bitr4g 554	1 |- (ph -> ((th <-> ps) <-> (th <-> ch)))

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

This theorem is referenced by:  bibi1d 618  bibi12d 628  biantr 741  euf 1382  ceqex 1882  sbc2or 1954  axrep1 2689  axrep2 2690  axrep3 2691  zfrepclf 2694  axsep2 2699  zfauscl 2700  copsexg 2787  isoeq1 3878  isoeq3 3880  caoprord 4048  aceq0 4710  aceq5 4720  axac 4725  zfcndrep 4946  zfcndac 4951  ltapq 5056  ltmpq 5057  ltasr 5189  pre-axltadd 5269  ltadd1t 5605  leadd1t 5607  ltmul1 5786  ltdiv1 5788  ltmul1t 5794  ltdiv1t 5813  clm4at 7036  eigret 9701  isded 10549  dedi 10550

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