Theorem bibi1d 619

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

Hypothesis

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

Assertion

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

Proof of Theorem bibi1d

Step	Hyp	Ref	Expression
1		bid.1	. . 3 |- (ph -> (ps <-> ch))
2	1	bibi2d 618	. 2 |- (ph -> ((th <-> ps) <-> (th <-> ch)))
3		bicom 520	. 2 |- ((ps <-> th) <-> (th <-> ps))
4		bicom 520	. 2 |- ((ch <-> th) <-> (th <-> ch))
5	2, 3, 4	3bitr4g 555	1 |- (ph -> ((ps <-> th) <-> (ch <-> th)))

Syntax hints:   -> wi 3   <-> wb 146

This theorem is referenced by:  pm4.22 622  bibi1 625  bibi12d 629  biass 744  eubid 1385  zfext2 1461  bm1.1 1462  eqeq1 1481  elabgt 1895  sbcabel 1996  sbcel12g 2011  axrep1 2694  isoeq2 3888  axacndlem4 4962  axacnd 4964  addcant 5352  lesub0t 5678  mulcant2 5688  mulcant2OLD 5689  mulcant 5690  mulcantOLD 5691  div11t 5765  expeq0t 6585  ismet 7798  ismsg 7800  msflem 7803  metreslem 7822  hvaddcant 8937  eigret 9761  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