Theorem bibi1d 618

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 617	. 2 |- (ph -> ((th <-> ps) <-> (th <-> ch)))
3		bicom 519	. 2 |- ((ps <-> th) <-> (th <-> ps))
4		bicom 519	. 2 |- ((ch <-> th) <-> (th <-> ch))
5	2, 3, 4	3bitr4g 554	1 |- (ph -> ((ps <-> th) <-> (ch <-> th)))

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

This theorem is referenced by:  pm4.22 621  bibi1 624  bibi12d 628  biass 743  eubid 1383  zfext2 1459  bm1.1 1460  eqeq1 1478  elabgt 1891  sbcabel 1992  sbcel12g 2007  axrep1 2689  isoeq2 3879  axacndlem4 4942  axacnd 4944  addcant 5332  lesub0t 5659  mulcant2 5668  mulcant 5669  div11t 5729  expeq0t 6525  ismet 7748  ismsg 7750  msflem 7753  metreslem 7774  hvaddcant 8876  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