Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  bibi1i Structured version   Visualization version   GIF version

Theorem bibi1i 327
 Description: Inference adding a biconditional to the right in an equivalence. (Contributed by NM, 26-May-1993.)
Hypothesis
Ref Expression
bibi2i.1 (𝜑𝜓)
Assertion
Ref Expression
bibi1i ((𝜑𝜒) ↔ (𝜓𝜒))

Proof of Theorem bibi1i
StepHypRef Expression
1 bicom 212 . 2 ((𝜑𝜒) ↔ (𝜒𝜑))
2 bibi2i.1 . . 3 (𝜑𝜓)
32bibi2i 326 . 2 ((𝜒𝜑) ↔ (𝜒𝜓))
4 bicom 212 . 2 ((𝜒𝜓) ↔ (𝜓𝜒))
51, 3, 43bitri 286 1 ((𝜑𝜒) ↔ (𝜓𝜒))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 196 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8 This theorem depends on definitions:  df-bi 197 This theorem is referenced by:  bibi12i  328  biluk  994  xorass  1508  hadbi  1577  hadnot  1581  sbrbis  2433  ssequn1  3816  symdifass  3886  asymref  5547  aceq1  8978  aceq0  8979  zfac  9320  zfcndac  9479  funcnvmptOLD  29595  hashreprin  30826  axacprim  31710  rp-fakeanorass  38175  rp-fakenanass  38177
 Copyright terms: Public domain W3C validator