Theorem bibi2i 669

Description: Inference adding a biconditional to the left in an equivalence. (The proof was shortened by Andrew Salmon, 7-May-2011.)

Hypothesis

Ref	Expression
bibi.a	|- (ph <-> ps)

Assertion

Ref	Expression
bibi2i	|- ((ch <-> ph) <-> (ch <-> ps))

Proof of Theorem bibi2i

Step	Hyp	Ref	Expression
1		bibi.a	. . . 4 |- (ph <-> ps)
2	1	imbi2i 202	. . 3 |- ((ch -> ph) <-> (ch -> ps))
3	1	imbi1i 203	. . 3 |- ((ph -> ch) <-> (ps -> ch))
4	2, 3	anbi12i 540	. 2 |- (((ch -> ph) /\ (ph -> ch)) <-> ((ch -> ps) /\ (ps -> ch)))
5		dfbi2 572	. 2 |- ((ch <-> ph) <-> ((ch -> ph) /\ (ph -> ch)))
6		dfbi2 572	. 2 |- ((ch <-> ps) <-> ((ch -> ps) /\ (ps -> ch)))
7	4, 5, 6	3bitr4i 200	1 |- ((ch <-> ph) <-> (ch <-> ps))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240

This theorem is referenced by:  bibi1i 671  bibi12i 672  pm4.71r 698  pm5.55 739  sblbis 1610  sbrbif 1612  sb8eu 1783  abeq2 1999  abid2f 2012  disj3 2918  euabsn 3095  axrep1 3429  axrep5 3433  axsep 3437  inex1 3452  axpr 3523  zfpair2 3525  sucel 3738  bnj89 12444  bnj100 12449  bnj99 12450  bnj142 12474  bnj145 12477  isprm3 13776  axrepprim 13786  bisym1 14243  assxor 14279  pm13.183 16373

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 164  df-an 242

Copyright terms: Public domain