HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem bibi2i 607
Description: Inference adding a biconditional to the left in an equivalence.
Hypothesis
Ref Expression
bibi.a |- (ph <-> ps)
Assertion
Ref Expression
bibi2i |- ((ch <-> ph) <-> (ch <-> ps))
Proof of Theorem bibi2i
StepHypRef Expression
1 bi 514 . 2 |- ((ch <-> ph) <-> ((ch -> ph) /\ (ph -> ch)))
2 bibi.a . . . 4 |- (ph <-> ps)
32imbi1i 186 . . 3 |- ((ph -> ch) <-> (ps -> ch))
43anbi2i 480 . 2 |- (((ch -> ph) /\ (ph -> ch)) <-> ((ch -> ph) /\ (ps -> ch)))
52imbi2i 185 . . . 4 |- ((ch -> ph) <-> (ch -> ps))
65anbi1i 481 . . 3 |- (((ch -> ph) /\ (ps -> ch)) <-> ((ch -> ps) /\ (ps -> ch)))
7 bi 514 . . 3 |- ((ch <-> ps) <-> ((ch -> ps) /\ (ps -> ch)))
86, 7bitr4 176 . 2 |- (((ch -> ph) /\ (ps -> ch)) <-> (ch <-> ps))
91, 4, 83bitr 177 1 |- ((ch <-> ph) <-> (ch <-> ps))
Colors of variables: wff set class
Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223
This theorem is referenced by:  bibi1i 608  bibi12i 609  pm4.71r 635  pm5.55 674  sblbis 1238  sbrbif 1240  abeq2 1565  disj3 2310  eusn 2442  axrep1 2689  axrep5 2693  axsep 2697  inex1 2711  axpr 2773  zfpair2 2775  sucel 3037
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