Theorem bibi1d 617

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 616	. 2 |- (ph -> ((th <-> ps) <-> (th <-> ch)))
3		bicom 518	. 2 |- ((ps <-> th) <-> (th <-> ps))
4		bicom 518	. 2 |- ((ch <-> th) <-> (th <-> ch))
5	2, 3, 4	3bitr4g 553	1 |- (ph -> ((ps <-> th) <-> (ch <-> th)))

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

This theorem is referenced by:  pm4.22 620  bibi1 623  bibi12d 627  biass 742  eubid 1378  zfext2 1454  bm1.1 1455  eqeq1 1473  elabgt 1886  sbcabel 1986  sbcel12g 2001  axrep1 2684  isoeq2 3873  axacndlem4 4934  axacnd 4936  addcant 5324  lesub0t 5651  mulcant2 5660  mulcant 5661  div11t 5721  expeq0t 6517  ismet 7737  ismsg 7739  msflem 7742  metreslem 7762  hvaddcant 8858  eigret 9678  isded 10513  dedi 10514

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