Theorem bibi2d 618

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 612	. . . 4 |- (ph -> ((th -> ps) <-> (th -> ch)))
3	2	anbi1d 617	. . 3 |- (ph -> (((th -> ps) /\ (ps -> th)) <-> ((th -> ch) /\ (ps -> th))))
4	1	imbi1d 613	. . . 4 |- (ph -> ((ps -> th) <-> (ch -> th)))
5	4	anbi2d 616	. . 3 |- (ph -> (((th -> ch) /\ (ps -> th)) <-> ((th -> ch) /\ (ch -> th))))
6	3, 5	bitrd 528	. 2 |- (ph -> (((th -> ps) /\ (ps -> th)) <-> ((th -> ch) /\ (ch -> th))))
7		dfbi2 514	. 2 |- ((th <-> ps) <-> ((th -> ps) /\ (ps -> th)))
8		dfbi2 514	. 2 |- ((th <-> ch) <-> ((th -> ch) /\ (ch -> th)))
9	6, 7, 8	3bitr4g 555	1 |- (ph -> ((th <-> ps) <-> (th <-> ch)))

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

This theorem is referenced by:  bibi1d 619  bibi12d 629  biantr 742  euf 1384  ceqex 1886  sbc2or 1958  axrep1 2694  axrep2 2695  axrep3 2696  zfrepclf 2699  axsep2 2704  zfauscl 2705  copsexg 2792  isoeq1 3887  isoeq3 3889  caoprord 4056  aceq0 4730  aceq5 4740  axac 4745  zfcndrep 4966  zfcndac 4971  ltapq 5076  ltmpq 5077  ltasr 5209  pre-axltadd 5289  ltadd1t 5623  leadd1t 5625  ltmul1 5822  ltdiv1 5824  ltmul1t 5830  ltdiv1t 5849  ltdiv1tOLD 5850  clm4at 7090  eigret 9761  ompfl3 10427  isded 10669  dedi 10670

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